Theorem ltexpq 3874

Description: Ordering on positive fractions in terms of existence of sum. Definition in Proposition 9-2.6 of [Gleason] p. 119.

Hypothesis

Ref	Expression
ltexpq.1	|- A e. V

Assertion

Ref	Expression
ltexpq	|- ((A e. Q. /\ B e. Q.) -> (A <Q B <-> E.x(A +Q x) = B))

Distinct variable group(s):   x,A   x,B

Proof of Theorem ltexpq

Step	Hyp	Ref	Expression
1		df-nq 3832	. . 3 |- Q. = ((N. X. N.)/. ~Q )
2		breq1 2065	. . . 4 |- ([<.y, z>.] ~Q = A -> ([<.y, z>.] ~Q <Q [<.w, v>.] ~Q <-> A <Q [<.w, v>.] ~Q ))
3		opreq1 3006	. . . . . 6 |- ([<.y, z>.] ~Q = A -> ([<.y, z>.] ~Q +Q x) = (A +Q x))
4	3	cleq1d 1109	. . . . 5 |- ([<.y, z>.] ~Q = A -> (([<.y, z>.] ~Q +Q x) = [<.w, v>.] ~Q <-> (A +Q x) = [<.w, v>.] ~Q ))
5	4	biexdv 936	. . . 4 |- ([<.y, z>.] ~Q = A -> (E.x([<.y, z>.] ~Q +Q x) = [<.w, v>.] ~Q <-> E.x(A +Q x) = [<.w, v>.] ~Q ))
6	2, 5	imbi12d 474	. . 3 |- ([<.y, z>.] ~Q = A -> (([<.y, z>.] ~Q <Q [<.w, v>.] ~Q -> E.x([<.y, z>.] ~Q +Q x) = [<.w, v>.] ~Q ) <-> (A <Q [<.w, v>.] ~Q -> E.x(A +Q x) = [<.w, v>.] ~Q )))
7		breq2 2066	. . . 4 |- ([<.w, v>.] ~Q = B -> (A <Q [<.w, v>.] ~Q <-> A <Q B))
8		cleq2 1110	. . . . 5 |- ([<.w, v>.] ~Q = B -> ((A +Q x) = [<.w, v>.] ~Q <-> (A +Q x) = B))
9	8	biexdv 936	. . . 4 |- ([<.w, v>.] ~Q = B -> (E.x(A +Q x) = [<.w, v>.] ~Q <-> E.x(A +Q x) = B))
10	7, 9	imbi12d 474	. . 3 |- ([<.w, v>.] ~Q = B -> ((A <Q [<.w, v>.] ~Q -> E.x(A +Q x) = [<.w, v>.] ~Q ) <-> (A <Q B -> E.x(A +Q x) = B)))
11		mulclpi 3815	. . . . . . . 8 |- ((y e. N. /\ v e. N.) -> (y .N v) e. N.)
12		mulclpi 3815	. . . . . . . 8 |- ((z e. N. /\ w e. N.) -> (z .N w) e. N.)
13	11, 12	anim12i 268	. . . . . . 7 |- (((y e. N. /\ v e. N.) /\ (z e. N. /\ w e. N.)) -> ((y .N v) e. N. /\ (z .N w) e. N.))
14	13	an42s 391	. . . . . 6 |- (((y e. N. /\ z e. N.) /\ (w e. N. /\ v e. N.)) -> ((y .N v) e. N. /\ (z .N w) e. N.))
15		ltexpi 3823	. . . . . 6 |- (((y .N v) e. N. /\ (z .N w) e. N.) -> ((y .N v) <N (z .N w) <-> E.u(u e. N. /\ ((y .N v) +N u) = (z .N w))))
16	14, 15	syl 12	. . . . 5 |- (((y e. N. /\ z e. N.) /\ (w e. N. /\ v e. N.)) -> ((y .N v) <N (z .N w) <-> E.u(u e. N. /\ ((y .N v) +N u) = (z .N w))))
17		pm3.26 256	. . . . . . . . . . . . 13 |- (((y e. N. /\ z e. N.) /\ (w e. N. /\ v e. N.)) -> (y e. N. /\ z e. N.))
18	17	adantr 306	. . . . . . . . . . . 12 |- ((((y e. N. /\ z e. N.) /\ (w e. N. /\ v e. N.)) /\ u e. N.) -> (y e. N. /\ z e. N.))
19		pm3.27 260	. . . . . . . . . . . . 13 |- ((((y e. N. /\ z e. N.) /\ (w e. N. /\ v e. N.)) /\ u e. N.) -> u e. N.)
20		pm3.27 260	. . . . . . . . . . . . . . . 16 |- ((y e. N. /\ z e. N.) -> z e. N.)
21		pm3.27 260	. . . . . . . . . . . . . . . 16 |- ((w e. N. /\ v e. N.) -> v e. N.)
22	20, 21	anim12i 268	. . . . . . . . . . . . . . 15 |- (((y e. N. /\ z e. N.) /\ (w e. N. /\ v e. N.)) -> (z e. N. /\ v e. N.))
23	22	adantr 306	. . . . . . . . . . . . . 14 |- ((((y e. N. /\ z e. N.) /\ (w e. N. /\ v e. N.)) /\ u e. N.) -> (z e. N. /\ v e. N.))
24		mulclpi 3815	. . . . . . . . . . . . . 14 |- ((z e. N. /\ v e. N.) -> (z .N v) e. N.)
25	23, 24	syl 12	. . . . . . . . . . . . 13 |- ((((y e. N. /\ z e. N.) /\ (w e. N. /\ v e. N.)) /\ u e. N.) -> (z .N v) e. N.)
26	19, 25	jca 236	. . . . . . . . . . . 12 |- ((((y e. N. /\ z e. N.) /\ (w e. N. /\ v e. N.)) /\ u e. N.) -> (u e. N. /\ (z .N v) e. N.))
27	18, 26	jca 236	. . . . . . . . . . 11 |- ((((y e. N. /\ z e. N.) /\ (w e. N. /\ v e. N.)) /\ u e. N.) -> ((y e. N. /\ z e. N.) /\ (u e. N. /\ (z .N v) e. N.)))
28	27	adantrr 312	. . . . . . . . . 10 |- ((((y e. N. /\ z e. N.) /\ (w e. N. /\ v e. N.)) /\ (u e. N. /\ ((y .N v) +N u) = (z .N w))) -> ((y e. N. /\ z e. N.) /\ (u e. N. /\ (z .N v) e. N.)))
29		addpipq 3848	. . . . . . . . . 10 |- (((y e. N. /\ z e. N.) /\ (u e. N. /\ (z .N v) e. N.)) -> ([<.y, z>.] ~Q +Q [<.u, (z .N v)>.] ~Q ) = [<.((y .N (z .N v)) +N (z .N u)), (z .N (z .N v))>.] ~Q )
30	28, 29	syl 12	. . . . . . . . 9 |- ((((y e. N. /\ z e. N.) /\ (w e. N. /\ v e. N.)) /\ (u e. N. /\ ((y .N v) +N u) = (z .N w))) -> ([<.y, z>.] ~Q +Q [<.u, (z .N v)>.] ~Q ) = [<.((y .N (z .N v)) +N (z .N u)), (z .N (z .N v))>.] ~Q )
31	20	ad2antll 320	. . . . . . . . . . . 12 |- ((((y e. N. /\ z e. N.) /\ (w e. N. /\ v e. N.)) /\ u e. N.) -> z e. N.)
32		addclpi 3814	. . . . . . . . . . . . 13 |- (((y .N v) e. N. /\ u e. N.) -> ((y .N v) +N u) e. N.)
33		pm3.26 256	. . . . . . . . . . . . . 14 |- ((y e. N. /\ z e. N.) -> y e. N.)
34	11, 33, 21	syl2an 349	. . . . . . . . . . . . 13 |- (((y e. N. /\ z e. N.) /\ (w e. N. /\ v e. N.)) -> (y .N v) e. N.)
35	32, 34	sylan 343	. . . . . . . . . . . 12 |- ((((y e. N. /\ z e. N.) /\ (w e. N. /\ v e. N.)) /\ u e. N.) -> ((y .N v) +N u) e. N.)
36	31, 35, 25	3jca 604	. . . . . . . . . . 11 |- ((((y e. N. /\ z e. N.) /\ (w e. N. /\ v e. N.)) /\ u e. N.) -> (z e. N. /\ ((y .N v) +N u) e. N. /\ (z .N v) e. N.))
37	36	adantrr 312	. . . . . . . . . 10 |- ((((y e. N. /\ z e. N.) /\ (w e. N. /\ v e. N.)) /\ (u e. N. /\ ((y .N v) +N u) = (z .N w))) -> (z e. N. /\ ((y .N v) +N u) e. N. /\ (z .N v) e. N.))
38		visset 1350	. . . . . . . . . . . 12 |- z e. V
39		oprex 3018	. . . . . . . . . . . 12 |- ((y .N v) +N u) e. V
40		oprex 3018	. . . . . . . . . . . 12 |- (z .N v) e. V
41	38, 39, 40	distrpqlem 3860	. . . . . . . . . . 11 |- ((z e. N. /\ ((y .N v) +N u) e. N. /\ (z .N v) e. N.) -> [<.(z .N ((y .N v) +N u)), (z .N (z .N v))>.] ~Q = [<.((y .N v) +N u), (z .N v)>.] ~Q )
42		visset 1350	. . . . . . . . . . . . . . . 16 |- y e. V
43		visset 1350	. . . . . . . . . . . . . . . 16 |- v e. V
44		visset 1350	. . . . . . . . . . . . . . . . 17 |- x e. V
45		visset 1350	. . . . . . . . . . . . . . . . 17 |- w e. V
46	44, 45	mulcompi 3818	. . . . . . . . . . . . . . . 16 |- (x .N w) = (w .N x)
47		visset 1350	. . . . . . . . . . . . . . . . 17 |- u e. V
48	45, 47	mulasspi 3819	. . . . . . . . . . . . . . . 16 |- ((x .N w) .N u) = (x .N (w .N u))
49	42, 38, 43, 46, 48	caopr12 3075	. . . . . . . . . . . . . . 15 |- (y .N (z .N v)) = (z .N (y .N v))
50	49	opreq1i 3009	. . . . . . . . . . . . . 14 |- ((y .N (z .N v)) +N (z .N u)) = ((z .N (y .N v)) +N (z .N u))
51		oprex 3018	. . . . . . . . . . . . . . 15 |- (y .N v) e. V
52	51, 47	distrpi 3820	. . . . . . . . . . . . . 14 |- (z .N ((y .N v) +N u)) = ((z .N (y .N v)) +N (z .N u))
53	50, 52	eqtr4 1122	. . . . . . . . . . . . 13 |- ((y .N (z .N v)) +N (z .N u)) = (z .N ((y .N v) +N u))
54		opeq1 1876	. . . . . . . . . . . . 13 |- (((y .N (z .N v)) +N (z .N u)) = (z .N ((y .N v) +N u)) -> <.((y .N (z .N v)) +N (z .N u)), (z .N (z .N v))>. = <.(z .N ((y .N v) +N u)), (z .N (z .N v))>.)
55	53, 54	ax-mp 6	. . . . . . . . . . . 12 |- <.((y .N (z .N v)) +N (z .N u)), (z .N (z .N v))>. = <.(z .N ((y .N v) +N u)), (