Theorem ltsopq 5055

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 5018	. . 3 |- Q. = ((N. X. N.)/. ~Q )
2		breq1 2617	. . . . 5 |- ([<.x, y>.] ~Q = f -> ([<.x, y>.] ~Q <Q [<.z, w>.] ~Q <-> f <Q [<.z, w>.] ~Q ))
3		eqeq1 1478	. . . . . . 7 |- ([<.x, y>.] ~Q = f -> ([<.x, y>.] ~Q = [<.z, w>.] ~Q <-> f = [<.z, w>.] ~Q ))
4		breq2 2618	. . . . . . 7 |- ([<.x, y>.] ~Q = f -> ([<.z, w>.] ~Q <Q [<.x, y>.] ~Q <-> [<.z, w>.] ~Q <Q f))
5	3, 4	orbi12d 626	. . . . . 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	negbid 610	. . . . 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 628	. . . 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 616	. . . . 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 2617	. . . . 5 |- ([<.x, y>.] ~Q = f -> ([<.x, y>.] ~Q <Q [<.v, u>.] ~Q <-> f <Q [<.v, u>.] ~Q ))
10	8, 9	imbi12d 625	. . . 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 627	. . 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 2618	. . . . 5 |- ([<.z, w>.] ~Q = g -> (f <Q [<.z, w>.] ~Q <-> f <Q g))
13		eqeq2 1481	. . . . . . 7 |- ([<.z, w>.] ~Q = g -> (f = [<.z, w>.] ~Q <-> f = g))
14		breq1 2617	. . . . . . 7 |- ([<.z, w>.] ~Q = g -> ([<.z, w>.] ~Q <Q f <-> g <Q f))
15	13, 14	orbi12d 626	. . . . . 6 |- ([<.z, w>.] ~Q = g -> ((f = [<.z, w>.] ~Q \/ [<.z, w>.] ~Q <Q f) <-> (f = g \/ g <Q f)))
16	15	negbid 610	. . . . 5 |- ([<.z, w>.] ~Q = g -> (-. (f = [<.z, w>.] ~Q \/ [<.z, w>.] ~Q <Q f) <-> -. (f = g \/ g <Q f)))
17	12, 16	bibi12d 628	. . . 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 2617	. . . . . 6 |- ([<.z, w>.] ~Q = g -> ([<.z, w>.] ~Q <Q [<.v, u>.] ~Q <-> g <Q [<.v, u>.] ~Q ))
19	12, 18	anbi12d 627	. . . . 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 612	. . . 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 627	. . 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 2618	. . . . . 6 |- ([<.v, u>.] ~Q = h -> (g <Q [<.v, u>.] ~Q <-> g <Q h))
23	22	anbi2d 615	. . . . 5 |- ([<.v, u>.] ~Q = h -> ((f <Q g /\ g <Q [<.v, u>.] ~Q ) <-> (f <Q g /\ g <Q h)))
24		breq2 2618	. . . . 5 |- ([<.v, u>.] ~Q = h -> (f <Q [<.v, u>.] ~Q <-> f <Q h))
25	23, 24	imbi12d 625	. . . 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 615	. . 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		ltsopi 4996	. . . . . . . . . 10 |- <N Or N.
28		sotric 2855	. . . . . . . . . 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))))
29	27, 28	mpan 694	. . . . . . . . 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))))
30		mulclpi 5001	. . . . . . . . 9 |- ((x e. N. /\ w e. N.) -> (x .N w) e. N.)
31		mulclpi 5001	. . . . . . . . 9 |- ((y e. N. /\ z e. N.) -> (y .N z) e. N.)
32	29, 30, 31	syl2an 454	. . . . . . . 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))))
33	32	an42s 509	. . . . . . 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))))
34		enqeceq 5027	. . . . . . . . 9 |- (((x e. N. /\ y e. N.) /\ (z e. N. /\ w e. N.)) -> ([<.x, y