Theorem ltsopq 6593

Description: 'Less than' is a strict ordering on positive fractions.

Assertion

Ref	Expression
ltsopq	|- <Q Or Q.

Proof of Theorem ltsopq

Step	Hyp	Ref	Expression
1		df-nq 6556	. . 3 |- Q. = ((N. X. N.)/. ~Q )
2		breq1 3510	. . . . 5 |- ([<.x, y>.] ~Q = f -> ([<.x, y>.] ~Q <Q [<.z, w>.] ~Q <-> f <Q [<.z, w>.] ~Q ))
3		eqeq1 2147	. . . . . . 7 |- ([<.x, y>.] ~Q = f -> ([<.x, y>.] ~Q = [<.z, w>.] ~Q <-> f = [<.z, w>.] ~Q ))
4		breq2 3511	. . . . . . 7 |- ([<.x, y>.] ~Q = f -> ([<.z, w>.] ~Q <Q [<.x, y>.] ~Q <-> [<.z, w>.] ~Q <Q f))
5	3, 4	orbi12d 762	. . . . . 6 |- ([<.x, y>.] ~Q = f -> (([<.x, y>.] ~Q = [<.z, w>.] ~Q \/ [<.z, w>.] ~Q <Q [<.x, y>.] ~Q ) <-> (f = [<.z, w>.] ~Q \/ [<.z, w>.] ~Q <Q f)))
6	5	notbid 746	. . . . 5 |- ([<.x, y>.] ~Q = f -> (-. ([<.x, y>.] ~Q = [<.z, w>.] ~Q \/ [<.z, w>.] ~Q <Q [<.x, y>.] ~Q ) <-> -. (f = [<.z, w>.] ~Q \/ [<.z, w>.] ~Q <Q f)))
7	2, 6	bibi12d 764	. . . 4 |- ([<.x, y>.] ~Q = f -> (([<.x, y>.] ~Q <Q [<.z, w>.] ~Q <-> -. ([<.x, y>.] ~Q = [<.z, w>.] ~Q \/ [<.z, w>.] ~Q <Q [<.x, y>.] ~Q )) <-> (f <Q [<.z, w>.] ~Q <-> -. (f = [<.z, w>.] ~Q \/ [<.z, w>.] ~Q <Q f))))
8	2	anbi1d 752	. . . . 5 |- ([<.x, y>.] ~Q = f -> (([<.x, y>.] ~Q <Q [<.z, w>.] ~Q /\ [<.z, w>.] ~Q <Q [<.v, u>.] ~Q ) <-> (f <Q [<.z, w>.] ~Q /\ [<.z, w>.] ~Q <Q [<.v, u>.] ~Q )))
9		breq1 3510	. . . . 5 |- ([<.x, y>.] ~Q = f -> ([<.x, y>.] ~Q <Q [<.v, u>.] ~Q <-> f <Q [<.v, u>.] ~Q ))
10	8, 9	imbi12d 761	. . . 4 |- ([<.x, y>.] ~Q = f -> ((([<.x, y>.] ~Q <Q [<.z, w>.] ~Q /\ [<.z, w>.] ~Q <Q [<.v, u>.] ~Q ) -> [<.x, y>.] ~Q <Q [<.v, u>.] ~Q ) <-> ((f <Q [<.z, w>.] ~Q /\ [<.z, w>.] ~Q <Q [<.v, u>.] ~Q ) -> f <Q [<.v, u>.] ~Q )))
11	7, 10	anbi12d 763	. . 3 |- ([<.x, y>.] ~Q = f -> ((([<.x, y>.] ~Q <Q [<.z, w>.] ~Q <-> -. ([<.x, y>.] ~Q = [<.z, w>.] ~Q \/ [<.z, w>.] ~Q <Q [<.x, y>.] ~Q )) /\ (([<.x, y>.] ~Q <Q [<.z, w>.] ~Q /\ [<.z, w>.] ~Q <Q [<.v, u>.] ~Q ) -> [<.x, y>.] ~Q <Q [<.v, u>.] ~Q )) <-> ((f <Q [<.z, w>.] ~Q <-> -. (f = [<.z, w>.] ~Q \/ [<.z, w>.] ~Q <Q f)) /\ ((f <Q [<.z, w>.] ~Q /\ [<.z, w>.] ~Q <Q [<.v, u>.] ~Q ) -> f <Q [<.v, u>.] ~Q ))))
12		breq2 3511	. . . . 5 |- ([<.z, w>.] ~Q = g -> (f <Q [<.z, w>.] ~Q <-> f <Q g))
13		eqeq2 2150	. . . . . . 7 |- ([<.z, w>.] ~Q = g -> (f = [<.z, w>.] ~Q <-> f = g))
14		breq1 3510	. . . . . . 7 |- ([<.z, w>.] ~Q = g -> ([<.z, w>.] ~Q <Q f <-> g <Q f))
15	13, 14	orbi12d 762	. . . . . 6 |- ([<.z, w>.] ~Q = g -> ((f = [<.z, w>.] ~Q \/ [<.z, w>.] ~Q <Q f) <-> (f = g \/ g <Q f)))
16	15	notbid 746	. . . . 5 |- ([<.z, w>.] ~Q = g -> (-. (f = [<.z, w>.] ~Q \/ [<.z, w>.] ~Q <Q f) <-> -. (f = g \/ g <Q f)))
17	12, 16	bibi12d 764	. . . 4 |- ([<.z, w>.] ~Q = g -> ((f <Q [<.z, w>.] ~Q <-> -. (f = [<.z, w>.] ~Q \/ [<.z, w>.] ~Q <Q f)) <-> (f <Q g <-> -. (f = g \/ g <Q f))))
18		breq1 3510	. . . . . 6 |- ([<.z, w>.] ~Q = g -> ([<.z, w>.] ~Q <Q [<.v, u>.] ~Q <-> g <Q [<.v, u>.] ~Q ))
19	12, 18	anbi12d 763	. . . . 5 |- ([<.z, w>.] ~Q = g -> ((f <Q [<.z, w>.] ~Q /\ [<.z, w>.] ~Q <Q [<.v, u>.] ~Q ) <-> (f <Q g /\ g <Q [<.v, u>.] ~Q )))
20	19	imbi1d 748	. . . 4 |- ([<.z, w>.] ~Q = g -> (((f <Q [<.z, w>.] ~Q /\ [<.z, w>.] ~Q <Q [<.v, u>.] ~Q ) -> f <Q [<.v, u>.] ~Q ) <-> ((f <Q g /\ g <Q [<.v, u>.] ~Q ) -> f <Q [<.v, u>.] ~Q )))
21	17, 20	anbi12d 763	. . 3 |- ([<.z, w>.] ~Q = g -> (((f <Q [<.z, w>.] ~Q <-> -. (f = [<.z, w>.] ~Q \/ [<.z, w>.] ~Q <Q f)) /\ ((f <Q [<.z, w>.] ~Q /\ [<.z, w>.] ~Q <Q [<.v, u>.] ~Q ) -> f <Q [<.v, u>.] ~Q )) <-> ((f <Q g <-> -. (f = g \/ g <Q f)) /\ ((f <Q g /\ g <Q [<.v, u>.] ~Q ) -> f <Q [<.v, u>.] ~Q ))))
22		breq2 3511	. . . . . 6 |- ([<.v, u>.] ~Q = h -> (g <Q [<.v, u>.] ~Q <-> g <Q h))
23	22	anbi2d 751	. . . . 5 |- ([<.v, u>.] ~Q = h -> ((f <Q g /\ g <Q [<.v, u>.] ~Q ) <-> (f <Q g /\ g <Q h)))
24		breq2 3511	. . . . 5 |- ([<.v, u>.] ~Q = h -> (f <Q [<.v, u>.] ~Q <-> f <Q h))
25	23, 24	imbi12d 761	. . . 4 |- ([<.v, u>.] ~Q = h -> (((f <Q g /\ g <Q [<.v, u>.] ~Q ) -> f <Q [<.v, u>.] ~Q ) <-> ((f <Q g /\ g <Q h) -> f <Q h)))
26	25	anbi2d 751	. . 3 |- ([<.v, u>.] ~Q = h -> (((f <Q g <-> -. (f = g \/ g <Q f)) /\ ((f <Q g /\ g <Q [<.v, u>.] ~Q ) -> f <Q [<.v, u>.] ~Q )) <-> ((f <Q g <-> -. (f = g \/ g <Q f)) /\ ((f <Q g /\ g <Q h) -> f <Q h))))
27		visset 2541	. . . . . . 7 |- x e. _V
28		visset 2541	. . . . . . 7 |- y e. _V
29		visset 2541	. . . . . . 7 |- z e. _V
30		visset 2541	. . . . . . 7 |- w e. _V
31	27, 28, 29, 30	ordpipq 6574	. . . . . 6 |- ([<.x, y>.] ~Q <Q [<.z, w>.] ~Q <-> (x .N w) <N (y .N z))
32		mulclpi 6539	. . . . . . . . 9 |- ((x e. N. /\ w e. N.) -> (x .N w) e. N.)
33		mulclpi 6539	. . . . . . . . 9 |- ((y e. N. /\ z e. N.) -> (y .N z) e. N.)
34		ltsopi 6534	. . . . . . . . . 10 |- <N Or N.
35		sotric 3774	. . . . . . . . . 10 |- (( <N Or N. /\ ((x .N w) e. N. /\ (y .N z) e. N.)) -> ((x .N w) <N (y .N z) <-> -. ((x .N w) = (y .N z) \/ (y .N z) <N (x .N w))))
36	34, 35	mpan 677	. . . . . . . . 9 |- (((x .N w) e. N. /\ (y .N z) e. N.) -> ((x .N w) <N (y .N z) <-> -. ((x .N w) = (y .N z) \/ (y .N z) <N (x .N w))))
37	32, 33, 36	syl2an 603	. . . . . . . 8 |- (((x e. N. /\ w e. N.) /\ (y e. N. /\ z e. N.)) -> ((x .N w) <N (y .N z) <-> -. ((x .N w) = (y .N z) \/ (y .N z) <N (x .N w))))
38	37	an42s 885	. . . . . . 7 |- (((x e. N. /\ y e. N.) /\ (z e. N. /\ w e. N.)) -> ((x .N w) <N (y .N z) <-> -. ((x .N w) = (y .N z) \/ (y .N z) <N (x .N w))))
39		enqeceq 6565	. . . . . . . . 9 |- (((x e. N. /\ y e. N.) /\ (z e. N. /\ w e. N.)) -> ([<.x, y>.] ~Q = [<.z, w>.] ~Q <-> (x .N w) = (y .N z)))
40	29, 30, 27, 28	ordpipq 6574	. . . . . . . . . . 11 |- ([<.z, w>.] ~Q <Q [<.x, y>.] ~Q <-> (z .N y) <N (w .N x))
41	29, 28	mulcompi 6542	. . . . . . . . . . . 12 |- (z .N y) = (y .N z)
42	30, 27	mulcompi 6542	. . . . . . . . . . . 12 |- (w .N x) = (x .N w)
43	41, 42	breq12i 3516	. . . . . . . . . . 11 |- ((z .N y) <N (w .N x) <-> (y .N z) <N (x .N w))
44	40, 43	bitri 279	. . . . . . . . . 10 |- ([<.z, w>.] ~Q <Q [<.x, y>.] ~Q <-> (y .N z) <N (x .N w))
45	44	a1i 8	. . . . . . . . 9 |- (((x e. N. /\ y e. N.) /\ (z e. N. /\ w e. N.)) -> ([<.z, w>.] ~Q <Q [<.x, y>.] ~Q <-> (y .N z) <N (x .N w)))
46	39, 45	orbi12d 762	. . . . . . . 8 |- (((x e. N. /\ y e. N.) /\ (z e. N. /\ w e. N.)) -> (([<.x, y>.] ~Q = [<.z, w>.] ~Q \/ [<.z, w>.] ~Q <Q [<.x, y>.] ~Q ) <-> ((x .N w) = (y .N z) \/ (y .N z) <N (x .N w))))
47	46	notbid 746	. . . . . . 7 |- (((x e. N. /\ y e. N.) /\ (z e. N. /\ w e. N.)) -> (-. ([<.x, y>.] ~Q = [<.z, w>.] ~Q \/ [<.z, w>.] ~Q <Q [<.x, y>.] ~Q ) <-> -. ((x .N w) = (y .N z) \/ (y .N z) <N (x .N w))))
48	38, 47	bitr4d 288	. . . . . 6 |- (((x e. N. /\ y e. N.) /\ (z e. N. /\ w e. N.)) -> ((x .N w) <N (y .N z) <-> -. ([<.x, y>.] ~Q = [<.z, w>.] ~Q \/ [<.z, w>.] ~Q <Q [<.x, y>.] ~Q )))
49	31, 48	syl5bb 721	. . . . 5 |- (((x e. N. /\ y e. N.) /\ (z e. N. /\ w e. N.)) -> ([<.x, y>.] ~Q <Q [<.z, w>.] ~Q <-> -. ([<.x, y>.] ~Q = [<.z, w>.] ~Q \/ [<.z, w>.] ~Q <Q [<.x, y>.] ~Q )))
50	49	3adant3 1140	. . . 4 |- (((x e. N. /\ y e. N.) /\ (z e. N. /\ w e. N.) /\ (v e. N. /\ u e. N.)) -> ([<.x, y>.] ~Q <Q [<.z, w>.] ~Q <-> -. ([<.x, y>.] ~Q = [<.z, w>.] ~Q \/ [<.z, w>.] ~Q <Q [<.x, y>.] ~Q )))
51		oprex 5003	. . . . . . . . . . 11 |- (x .N w) e. _V
52		oprex 5003	. . . . . . . . . . 11 |- (y .N z) e. _V
53		visset 2541	. . . . . . . . . . . 12 |- f e. _V
54		visset 2541	. . . . . . . . . . . 12 |- g e. _V
55	53, 54	ltmpi 6549	. . . . . . . . . . 11 |- (h e. N. -> (f <N g <-> (h .N f) <N (h .N g)))
56		visset 2541	. . . . . . . . . . 11 |- u e. _V
57	53, 54	mulcompi 6542	. . . . . . . . . . 11 |- (f .N g) = (g .N f)
58	51, 52, 55, 56, 57	caoprord2 5083	. . . . . . . . . 10 |- (u e. N. -> ((x .N w) <N (y .N z) <-> ((x .N w) .N u) <N ((y .N z) .N u)))
59	30, 56	mulasspi 6543	. . . . . . . . . . 11 |- ((x .N w) .N u) = (x .N (w .N u))
60	29, 56	mulasspi 6543	. . . . . . . . . . 11 |- ((y .N z) .N u) = (y .N (z .N u))
61	59, 60	breq12i 3516	. . . . . . . . . 10 |- (((x .N w) .N u) <N ((y .N z) .N u) <-> (x .N (w .N u)) <N (y .N (z .N u)))
62	58, 61	syl6bb 729	. . . . . . . . 9 |- (u e. N. -> ((x .N w) <N (y .N z) <-> (x .N (w .N u)) <N (y .N (z .N u))))
63	31, 62	syl5bb 721	. . . . . . . 8 |- (u e. N. -> ([<.x, y>.] ~Q <Q [<.z, w>.] ~Q <-> (x .N (w .N u)) <N (y .N (z .N u))))
64		visset 2541	. . . . . . . . . 10 |- v e. _V
65	29, 30, 64, 56	ordpipq 6574	. . . . . . . . 9 |- ([<.z, w>.] ~Q <Q [<.v, u>.] ~Q <-> (z .N u) <N (w .N v))
66		oprex 5003	. . . . . . . . . 10 |- (z .N u) e. _V
67		oprex 5003	. . . . . . . . . 10 |- (w .N v) e. _V
68	66, 67	ltmpi 6549	. . . . . . . . 9 |- (y e. N. -> ((z .N u) <N (w .N v) <-> (y .N (z .N u)) <N (y .N (w .N v))))
69	65, 68	syl5bb 721	. . . . . . . 8 |- (y e. N. -> ([<.z, w>.] ~Q <Q [<.v, u>.] ~Q <-> (y .N (z .N u)) <N (y .N (w .N v))))
70	63, 69	bi2anan9r 951	. . . . . . 7 |- ((y e. N. /\ u e. N.) -> (([<.x, y>.] ~Q <Q [<.z, w>.] ~Q /\ [<.z, w>.] ~Q <Q [<.v, u>.] ~Q ) <-> ((x .N (w .N u)) <N (y .N (z .N u)) /\ (y .N (z .N u)) <N (y .N (w .N v)))))
71		oprex 5003	. . . . . . . . 9 |- (x .N (w .N u)) e. _V
72		ltrelpi 6535	. . . . . . . . 9 |- <N C_ (N. X. N.)
73		oprex 5003	. . . . . . . . 9 |- (y .N (z .N u)) e. _V
74		oprex 5003	. . . . . . . . 9 |- (y .N (w .N v)) e. _V
75	71, 34, 72, 73, 74	sotri 4427	. . . . . . . 8 |- (((x .N (w .N u)) <N (y .N (z .N u)) /\ (y .N (z .N u)) <N (y .N (w .N v))) -> (x .N (w .N u)) <N (y .N (w .N v)))
76		oprex 5003	. . . . . . . . . 10 |- (x .N u) e. _V
77		dmmulpi 6537	. . . . . . . . . 10 |- dom .N = (N. X. N.)
78		0npi 6528	. . . . . . . . . 10 |- -. (/) e. N.
79		oprex 5003	. . . . . . . . . . 11 |- (y .N v) e. _V
80	76, 79	ltmpi 6549	. . . . . . . . . 10 |- (w e. N. -> ((x .N u) <N (y .N v) <-> (w .N (x .N u)) <N (w .N (y .N v))))
81	76, 77, 72, 78, 80	ndmordi 5077	. . . . . . . . 9 |- ((w .N (x .N u)) <N (w .N (y .N v)) -> (x .N u) <N (y .N v))
82		visset 2541	. . . . . . . . . . . 12 |- h e. _V
83	54, 82	mulasspi 6543	. . . . . . . . . . 11 |- ((f .N g) .N h) = (f .N (g .N h))
84	27, 30, 56, 57, 83	caopr12 5087	. . . . . . . . . 10 |- (x .N (w .N u)) = (w .N (x .N u))
85	28, 30, 64, 57, 83	caopr12 5087	. . . . . . . . . 10 |- (y .N (w .N v)) = (w .N (y .N v))
86	84, 85	breq12i 3516	. . . . . . . . 9 |- ((x .N (w .N u)) <N (y .N (w .N v)) <-> (w .N (x .N u)) <N (w .N (y .N v)))
87	27, 28, 64, 56	ordpipq 6574	. . . . . . . . 9 |- ([<.x, y>.] ~Q <Q [<.v, u>.] ~Q <-> (x .N u) <N (y .N v))
88	81, 86, 87	3imtr4i 328	. . . . . . . 8 |- ((x .N (w .N u)) <N (y .N (w .N v)) -> [<.x, y>.] ~Q <Q [<.v, u>.] ~Q )
89	75, 88	syl 13	. . . . . . 7 |- (((x .N (w .N u)) <N (y .N (z .N u)) /\ (y .N (z .N u)) <N (y .N (w .N v))) -> [<.x, y>.] ~Q <Q [<.v, u>.] ~Q )
90	70, 89	syl6bi 263	. . . . . 6 |- ((y e. N. /\ u e. N.) -> (([<.x, y>.] ~Q <Q [<.z, w>.] ~Q /\ [<.z, w>.] ~Q <Q [<.v, u>.] ~Q ) -> [<.x, y>.] ~Q <Q [<.v, u>.] ~Q ))
91	90	ad2ant2l 806	. . . . 5 |- (((x e. N. /\ y e. N.) /\ (v e. N. /\ u e. N.)) -> (([<.x, y>.] ~Q <Q [<.z, w>.] ~Q /\ [<.z, w>.] ~Q <Q [<.v, u>.] ~Q ) -> [<.x, y>.] ~Q <Q [<.v, u>.] ~Q ))
92	91	3adant2 1139	. . . 4 |- (((x e. N. /\ y e. N.) /\ (z e. N. /\ w e. N.) /\ (v e. N. /\ u e. N.)) -> (([<.x, y>.] ~Q <Q [<.z, w>.] ~Q /\ [<.z, w>.] ~Q <Q [<.v, u>.] ~Q ) -> [<.x, y>.] ~Q <Q [<.v, u>.] ~Q ))
93	50, 92	jca 494	. . 3 |- (((x e. N. /\ y e. N.) /\ (z e. N. /\ w e. N.) /\ (v e. N. /\ u e. N.)) -> (([<.x, y>.] ~Q <Q [<.z, w>.] ~Q <-> -. ([<.x, y>.] ~Q = [<.z, w>.] ~Q \/ [<.z, w>.] ~Q <Q [<.x, y>.] ~Q )) /\ (([<.x, y>.] ~Q <Q [<.z, w>.] ~Q /\ [<.z, w>.] ~Q <Q [<.v, u>.] ~Q ) -> [<.x, y>.] ~Q <Q [<.v, u>.] ~Q )))
94	1, 11, 21, 26, 93	3ecoptocl 5525	. 2 |- ((f e. Q. /\ g e. Q. /\ h e. Q.) -> ((f <Q g <-> -. (f = g \/ g <Q f)) /\ ((f <Q g /\ g <Q h) -> f <Q h)))
95	94	so 3778	1 |- <Q Or Q.

Syntax hints:  -. wn 2   -> wi 3   <-> wb 219   \/ wo 336   /\ wa 337   /\ w3a 1102   = wceq 1586   e. wcel 1588  <.cop 3240   class class class wbr 3507   Or wor 3751  (class class class)co 4981  [cec 5477  N.cnpi 6490   .N cmi 6492   <N clti 6493   ~Q ceq 6496  Q.cnq 6497   <Q cltq 6502

This theorem is referenced by:  ltrpq 6603  prub 6616  genpnnp 6626  1pr 6635  distrlem4pr 6648  prlem934 6657  ltexprlem4 6663  reclem2pr 6675  reclem4pr 6677

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-rep 3596  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929  ax-inf2 5964

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3or 1103  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-ral 2359  df-rex 2360  df-reu 2361  df-rab 2362  df-v 2540  df-sbc 2700  df-csb 2774  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-pss 2838  df-nul 3083  df-if 3181  df-pw 3229  df-sn 3242  df-pr 3243  df-tp 3245  df-op 3246  df-uni 3367  df-int 3401  df-iun 3438  df-br 3508  df-opab 3566  df-tr 3580  df-eprel 3744  df-id 3747  df-po 3752  df-so 3764  df-fr 3782  df-we 3798  df-ord 3814  df-on 3815  df-lim 3816  df-suc 3817  df-om 4086  df-xp 4133  df-rel 4134  df-cnv 4135  df-co 4136  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fun 4141  df-fn 4142  df-f 4143  df-fv 4147  df-opr 4983  df-oprab 4984  df-1st 5126  df-2nd 5127  df-rdg 5304  df-1o 5344  df-oadd 5346  df-omul 5347  df-er 5479  df-ec 5481  df-qs 5484  df-ni 6518  df-mi 6520  df-lti 6521  df-enq 6555  df-nq 6556  df-ltq 6560

Copyright terms: Public domain