Theorem ltapq 3870

Description: Ordering property of addition for positive fractions. Proposition 9-2.6(ii) of [Gleason] p. 120.

Hypotheses

Ref	Expression
ltapq.1	|- A e. V
ltapq.2	|- B e. V

Assertion

Ref	Expression
ltapq	|- (C e. Q. -> (A <Q B <-> (C +Q A) <Q (C +Q B)))

Proof of Theorem ltapq

Step	Hyp	Ref	Expression
1		ltapq.2	. 2 |- B e. V
2		dmaddpq 3853	. 2 |- dom +Q = (Q. X. Q.)
3		ltapq.1	. 2 |- A e. V
4		ltrelpq 3845	. 2 |- <Q (_ (Q. X. Q.)
5		0npq 3844	. 2 |- -. (/) e. Q.
6		df-nq 3832	. . 3 |- Q. = ((N. X. N.)/. ~Q )
7		breq1 2065	. . . 4 |- ([<.x, y>.] ~Q = A -> ([<.x, y>.] ~Q <Q [<.z, w>.] ~Q <-> A <Q [<.z, w>.] ~Q ))
8		opreq2 3007	. . . . 5 |- ([<.x, y>.] ~Q = A -> ([<.v, u>.] ~Q +Q [<.x, y>.] ~Q ) = ([<.v, u>.] ~Q +Q A))
9	8	breq1d 2071	. . . 4 |- ([<.x, y>.] ~Q = A -> (([<.v, u>.] ~Q +Q [<.x, y>.] ~Q ) <Q ([<.v, u>.] ~Q +Q [<.z, w>.] ~Q ) <-> ([<.v, u>.] ~Q +Q A) <Q ([<.v, u>.] ~Q +Q [<.z, w>.] ~Q )))
10	7, 9	bibi12d 477	. . 3 |- ([<.x, y>.] ~Q = A -> (([<.x, y>.] ~Q <Q [<.z, w>.] ~Q <-> ([<.v, u>.] ~Q +Q [<.x, y>.] ~Q ) <Q ([<.v, u>.] ~Q +Q [<.z, w>.] ~Q )) <-> (A <Q [<.z, w>.] ~Q <-> ([<.v, u>.] ~Q +Q A) <Q ([<.v, u>.] ~Q +Q [<.z, w>.] ~Q ))))
11		breq2 2066	. . . 4 |- ([<.z, w>.] ~Q = B -> (A <Q [<.z, w>.] ~Q <-> A <Q B))
12		opreq2 3007	. . . . 5 |- ([<.z, w>.] ~Q = B -> ([<.v, u>.] ~Q +Q [<.z, w>.] ~Q ) = ([<.v, u>.] ~Q +Q B))
13	12	breq2d 2072	. . . 4 |- ([<.z, w>.] ~Q = B -> (([<.v, u>.] ~Q +Q A) <Q ([<.v, u>.] ~Q +Q [<.z, w>.] ~Q ) <-> ([<.v, u>.] ~Q +Q A) <Q ([<.v, u>.] ~Q +Q B)))
14	11, 13	bibi12d 477	. . 3 |- ([<.z, w>.] ~Q = B -> ((A <Q [<.z, w>.] ~Q <-> ([<.v, u>.] ~Q +Q A) <Q ([<.v, u>.] ~Q +Q [<.z, w>.] ~Q )) <-> (A <Q B <-> ([<.v, u>.] ~Q +Q A) <Q ([<.v, u>.] ~Q +Q B))))
15		opreq1 3006	. . . . 5 |- ([<.v, u>.] ~Q = C -> ([<.v, u>.] ~Q +Q A) = (C +Q A))
16		opreq1 3006	. . . . 5 |- ([<.v, u>.] ~Q = C -> ([<.v, u>.] ~Q +Q B) = (C +Q B))
17	15, 16	breq12d 2073	. . . 4 |- ([<.v, u>.] ~Q = C -> (([<.v, u>.] ~Q +Q A) <Q ([<.v, u>.] ~Q +Q B) <-> (C +Q A) <Q (C +Q B)))
18	17	bibi2d 470	. . 3 |- ([<.v, u>.] ~Q = C -> ((A <Q B <-> ([<.v, u>.] ~Q +Q A) <Q ([<.v, u>.] ~Q +Q B)) <-> (A <Q B <-> (C +Q A) <Q (C +Q B))))
19		mulclpi 3815	. . . . . . . . . . . . 13 |- ((u e. N. /\ u e. N.) -> (u .N u) e. N.)
20		oprex 3018	. . . . . . . . . . . . . 14 |- (x .N w) e. V
21		oprex 3018	. . . . . . . . . . . . . 14 |- (y .N z) e. V
22	20, 21	ltmpi 3825	. . . . . . . . . . . . 13 |- ((u .N u) e. N. -> ((x .N w) <N (y .N z) <-> ((u .N u) .N (x .N w)) <N ((u .N u) .N (y .N z))))
23	19, 22	syl 12	. . . . . . . . . . . 12 |- ((u e. N. /\ u e. N.) -> ((x .N w) <N (y .N z) <-> ((u .N u) .N (x .N w)) <N ((u .N u) .N (y .N z))))
24	23	anidms 332	. . . . . . . . . . 11 |- (u e. N. -> ((x .N w) <N (y .N z) <-> ((u .N u) .N (x .N w)) <N ((u .N u) .N (y .N z))))
25	24	ad2antrl 322	. . . . . . . . . 10 |- (((v e. N. /\ y e. N.) /\ (u e. N. /\ w e. N.)) -> ((x .N w) <N (y .N z) <-> ((u .N u) .N (x .N w)) <N ((u .N u) .N (y .N z))))
26		mulclpi 3815	. . . . . . . . . . . . 13 |- ((v e. N. /\ y e. N.) -> (v .N y) e. N.)
27		mulclpi 3815	. . . . . . . . . . . . 13 |- ((u e. N. /\ w e. N.) -> (u .N w) e. N.)
28	26, 27	anim12i 268	. . . . . . . . . . . 12 |- (((v e. N. /\ y e. N.) /\ (u e. N. /\ w e. N.)) -> ((v .N y) e. N. /\ (u .N w) e. N.))
29		mulclpi 3815	. . . . . . . . . . . 12 |- (((v .N y) e. N. /\ (u .N w) e. N.) -> ((v .N y) .N (u .N w)) e. N.)
30		oprex 3018	. . . . . . . . . . . . 13 |- ((u .N x) .N (u .N w)) e. V
31		oprex 3018	. . . . . . . . . . . . 13 |- ((u .N y) .N (u .N z)) e. V
32	30, 31	ltapi 3824	. . . . . . . . . . . 12 |- (((v .N y) .N (u .N w)) e. N. -> (((u .N x) .N (u .N w)) <N ((u .N y) .N (u .N z)) <-> (((v .N y) .N (u .N w)) +N ((u .N x) .N (u .N w))) <N (((v .N y) .N (u .N w)) +N ((u .N y) .N (u .N z)))))
33	28, 29, 32	3syl 21	. . . . . . . . . . 11 |- (((v e. N. /\ y e. N.) /\ (u e. N. /\ w e. N.)) -> (((u .N x) .N (u .N w)) <N ((u .N y) .N (u .N z)) <-> (((v .N y) .N (u .N w)) +N ((u .N x) .N (u .N w))) <N (((v .N y) .N (u .N w)) +N ((u .N y) .N (u .N z)))))
34		visset 1350	. . . . . . . . . . . . 13 |- u e. V
35		visset 1350	. . . . . . . . . . . . 13 |- x e. V
36		visset 1350	. . . . . . . . . . . . . 14 |- f e. V
37		visset 1350	. . . . . . . . . . . . . 14 |- g e. V
38	36, 37	mulcompi 3818	. . . . . . . . . . . . 13 |- (f .N g) = (g .N f)
39		visset 1350	. . . . . . . . . . . . . 14 |- h e. V
40	37, 39	mulasspi 3819	. . . . . . . . . . . . 13 |- ((f .N g) .N h) = (f .N (g .N h))
41		visset 1350	. . . . . . . . . . . . 13 |- w e. V
42	34, 34, 35, 38, 40, 41	caopr4 3078	. . . . . . . . . . . 12 |- ((u .N u) .N (x .N w)) = ((u .N x) .N (u .N w))
43		visset 1350	. . . . . . . . . . . . 13 |- y e. V
44		visset 1350	. . . . . . . . . . . . 13 |- z e. V
45	34, 34, 43, 38, 40, 44	caopr4 3078	. . . . . . . . . . . 12 |- ((u .N u) .N (y .N z)) = ((u .N y) .N (u .N z))
46	42, 45	breq12i 2070	. . . . . . . . . . 11 |- (((u .N u) .N (x .N w)) <N ((u .N u) .N (y .N z)) <-> ((u .N x) .N (u .N w)) <N ((u .N y) .N (u .N z)))
47		oprex 3018	. . . . . . . . . . . . 13 |- (v .N y) e. V
48		oprex 3018	. . . . . . . . . . . . 13 |- (u .N x) e. V
49		oprex 3018	. . . . . . . . . . . . 13 |- (u .N w) e. V
50	37, 39	distrpi 3820	. . . . . . . . . . . . 13 |- (f .N (g +N h)) = ((f .N g) +N (f .N h))
51	47, 48, 49, 38, 50	caoprdistrr 3081	. . . . . . . . . . . 12 |- (((v .N y) +N (u .N x)) .N (u .N w)) = (((v .N y) .N (u .N w)) +N ((u .N x) .N (u .N w)))
52		oprex 3018	. . . . . . . . . . . . . 14 |- (v .N w) e. V
53		oprex 3018	. . . . . . . . . . . . . 14 |- (u .N z) e. V
54	52, 53	distrpi 3820	. . . . . . . . . . . . 13 |- ((u .N y) .N ((v .N w) +N (u .N z))) = (((u .N y) .N (v .N w)) +N ((u .N y) .N (u .N z)))
55		visset 1350	. . . . . . . . . . . . . . 15 |- v e. V
56	34, 43, 55, 38, 40, 41	caopr411 3079	. . . . . . . . . . . . . 14 |- ((u .N y) .N (v .N w)) = ((v .N y) .N (u .N w))
57	56	opreq1i 3009	. . . . . . . . . . . . 13 |- (((u .N y) .N (v .N w)) +N ((u .N y) .N (u .N z))) = (((v .N y) .N (u .N w)) +N ((u .N y) .N (u .N z)))
58	54, 57	eqtr 1119	. . . . . . . . . . . 12 |- ((u .N y) .N ((v .N w) +N (u .N z))) = (((v .N y) .N (u .N w)) +N ((u .N y) .N (u .N z)))
59	51, 58	breq12i 2070	. . . . . . . . . . 11 |- ((((v .N y) +N (u .N x)) .N (u .N w)) <N ((u .N y) .N ((v .N w) +N (u .N z))) <-> (((v .N y) .N (u .N w)) +N ((u .N x) .N (u .N w))) <N (((v .N y) .N (u .N w)) +N ((u .N y) .N (u .N z))))
60	33, 46, 59	3bitr4g 428	. . . . . . . . . 10 |- (((v e. N. /\ y e. N.) /\ (u e. N. /\ w e. N.)) -> (((u .N u) .N (