Theorem ltexpq 5092

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 groups:   x,A   x,B

Proof of Theorem ltexpq

Step	Hyp	Ref	Expression
1		df-nq 5050	. . 3 |- Q. = ((N. X. N.)/. ~Q )
2		breq1 2627	. . . 4 |- ([<.y, z>.] ~Q = A -> ([<.y, z>.] ~Q <Q [<.w, v>.] ~Q <-> A <Q [<.w, v>.] ~Q ))
3		opreq1 3974	. . . . . 6 |- ([<.y, z>.] ~Q = A -> ([<.y, z>.] ~Q +Q x) = (A +Q x))
4	3	eqeq1d 1486	. . . . 5 |- ([<.y, z>.] ~Q = A -> (([<.y, z>.] ~Q +Q x) = [<.w, v>.] ~Q <-> (A +Q x) = [<.w, v>.] ~Q ))
5	4	exbidv 1281	. . . 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 628	. . 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 2628	. . . 4 |- ([<.w, v>.] ~Q = B -> (A <Q [<.w, v>.] ~Q <-> A <Q B))
8		eqeq2 1487	. . . . 5 |- ([<.w, v>.] ~Q = B -> ((A +Q x) = [<.w, v>.] ~Q <-> (A +Q x) = B))
9	8	exbidv 1281	. . . 4 |- ([<.w, v>.] ~Q = B -> (E.x(A +Q x) = [<.w, v>.] ~Q <-> E.x(A +Q x) = B))
10	7, 9	imbi12d 628	. . 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 5033	. . . . . . . 8 |- ((y e. N. /\ v e. N.) -> (y .N v) e. N.)
12		mulclpi 5033	. . . . . . . 8 |- ((z e. N. /\ w e. N.) -> (z .N w) e. N.)
13	11, 12	anim12i 333	. . . . . . 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 511	. . . . . 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 5041	. . . . . 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 10	. . . . 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		simpll 414	. . . . . . . . . . . 12 |- ((((y e. N. /\ z e. N.) /\ (w e. N. /\ v e. N.)) /\ u e. N.) -> (y e. N. /\ z e. N.))
18		pm3.27 323	. . . . . . . . . . . . 13 |- ((((y e. N. /\ z e. N.) /\ (w e. N. /\ v e. N.)) /\ u e. N.) -> u e. N.)
19		pm3.27 323	. . . . . . . . . . . . . . . 16 |- ((y e. N. /\ z e. N.) -> z e. N.)
20		pm3.27 323	. . . . . . . . . . . . . . . 16 |- ((w e. N. /\ v e. N.) -> v e. N.)
21	19, 20	anim12i 333	. . . . . . . . . . . . . . 15 |- (((y e. N. /\ z e. N.) /\ (w e. N. /\ v e. N.)) -> (z e. N. /\ v e. N.))
22	21	adantr 391	. . . . . . . . . . . . . 14 |- ((((y e. N. /\ z e. N.) /\ (w e. N. /\ v e. N.)) /\ u e. N.) -> (z e. N. /\ v e. N.))
23		mulclpi 5033	. . . . . . . . . . . . . 14 |- ((z e. N. /\ v e. N.) -> (z .N v) e. N.)
24	22, 23	syl 10	. . . . . . . . . . . . 13 |- ((((y e. N. /\ z e. N.) /\ (w e. N. /\ v e. N.)) /\ u e. N.) -> (z .N v) e. N.)
25	18, 24	jca 288	. . . . . . . . . . . 12 |- ((((y e. N. /\ z e. N.) /\ (w e. N. /\ v e. N.)) /\ u e. N.) -> (u e. N. /\ (z .N v) e. N.))
26	17, 25	jca 288	. . . . . . . . . . 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.)))
27	26	adantrr 397	. . . . . . . . . 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.)))
28		addpipq 5066	. . . . . . . . . 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 )
29	27, 28	syl 10	. . . . . . . . 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 )
30	19	ad2antrr 406	. . . . . . . . . . . 12 |- ((((y e. N. /\ z e. N.) /\ (w e. N. /\ v e. N.)) /\ u e. N.) -> z e. N.)
31		addclpi 5032	. . . . . . . . . . . . 13 |- (((y .N v) e. N. /\ u e. N.) -> ((y .N v) +N u) e. N.)
32	11	ad2ant2rl 413	. . . . . . . . . . . . 13 |- (((y e. N. /\ z e. N.) /\ (w e. N. /\ v e. N.)) -> (y .N v) e. N.)
33	31, 32	sylan 450	. . . . . . . . . . . 12 |- ((((y e. N. /\ z e. N.) /\ (w e. N. /\ v e. N.)) /\ u e. N.) -> ((y .N v) +N u) e. N.)
34	30, 33, 24	3jca 821	. . . . . . . . . . 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.))
35	34	adantrr 397	. . . . . . . . . 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.))
36		visset 1816	. . . . . . . . . . . 12 |- z e. V
37		oprex 3989	. . . . . . . . . . . 12 |- ((y .N v) +N u) e. V
38		oprex 3989	. . . . . . . . . . . 12 |- (z .N v) e. V
39	36, 37, 38	distrpqlem 5078	. . . . . . . . . . 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 )
40		visset 1816	. . . . . . . . . . . . . . . 16 |- y e. V
41		visset 1816	. . . . . . . . . . . . . . . 16 |- v e. V
42		visset 1816	. . . . . . . . . . . . . . . . 17 |- x e. V
43		visset 1816	. . . . . . . . . . . . . . . . 17 |- w e. V
44	42, 43	mulcompi 5036	. . . . . . . . . . . . . . . 16 |- (x .N w) = (w .N x)
45		visset 1816	. . . . . . . . . . . . . . . . 17 |- u e. V
46	43, 45	mulasspi 5037	. . . . . . . . . . . . . . . 16 |- ((x .N w) .N u) = (x .N (w .N u))
47	40, 36, 41, 44, 46	caopr12 4067	. . . . . . . . . . . . . . 15 |- (y .N (z .N v)) = (z .N (y .N v))
48	47	opreq1i 3977	. . . . . . . . . . . . . 14 |- ((y .N (z .N v)) +N (z .N u)) = ((z .N (y .N v)) +N (z .N u))
49		oprex 3989	. . . . . . . . . . . . . . 15 |- (y .N v) e. V
50	49, 45	distrpi 5038	. . . . . . . . . . . . . 14 |- (z .N ((y .N v) +N u)) = ((z .N (y .N v)) +N (z .N u))
51	48, 50	eqtr4 1501	. . . . . . . . . . . . 13 |- ((y .N (z .N v)) +N (z .N u)) = (z .N ((y .N v) +N u))
52	51	opeq1i 2494	. . . . . . . . . . . 12 |- <.((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))>.
53		eceq2 4284	. . . . . . . . . . . 12 |- (<.((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))>. -> [<.((y .N (z .N v)) +N (z .N u)