Theorem climmullem5 7124

Description: Lemma for climmul 7128. Instead of the infimum that Gleason uses (bottom of p. 170), we use recrecltt 5902 to give us a number smaller than both a given number and 1. Warning: The HTML proof page is 1/2 megabyte in size.

Assertion

Ref	Expression
climmullem5	|- (((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC) /\ (v e. RR /\ 0 < v)) -> (((abs` (F - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) /\ (abs` (G - B)) < ((v / 2) / (1 + (abs` A)))) -> (abs` ((F x. G) - (A x. B))) < v))

Proof of Theorem climmullem5

Step	Hyp	Ref	Expression
1		subdit 5427	. . . . . . . . . . . 12 |- ((F e. CC /\ G e. CC /\ B e. CC) -> (F x. (G - B)) = ((F x. G) - (F x. B)))
2	1	3expa 833	. . . . . . . . . . 11 |- (((F e. CC /\ G e. CC) /\ B e. CC) -> (F x. (G - B)) = ((F x. G) - (F x. B)))
3	2	adantrl 394	. . . . . . . . . 10 |- (((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC)) -> (F x. (G - B)) = ((F x. G) - (F x. B)))
4		subdirt 5428	. . . . . . . . . . . 12 |- ((F e. CC /\ A e. CC /\ B e. CC) -> ((F - A) x. B) = ((F x. B) - (A x. B)))
5	4	3expb 834	. . . . . . . . . . 11 |- ((F e. CC /\ (A e. CC /\ B e. CC)) -> ((F - A) x. B) = ((F x. B) - (A x. B)))
6	5	adantlr 393	. . . . . . . . . 10 |- (((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC)) -> ((F - A) x. B) = ((F x. B) - (A x. B)))
7	3, 6	opreq12d 3978	. . . . . . . . 9 |- (((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC)) -> ((F x. (G - B)) + ((F - A) x. B)) = (((F x. G) - (F x. B)) + ((F x. B) - (A x. B))))
8		npncant 5400	. . . . . . . . . 10 |- (((F x. G) e. CC /\ (F x. B) e. CC /\ (A x. B) e. CC) -> (((F x. G) - (F x. B)) + ((F x. B) - (A x. B))) = ((F x. G) - (A x. B)))
9		axmulcl 5273	. . . . . . . . . . 11 |- ((F e. CC /\ G e. CC) -> (F x. G) e. CC)
10	9	adantr 389	. . . . . . . . . 10 |- (((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC)) -> (F x. G) e. CC)
11		axmulcl 5273	. . . . . . . . . . 11 |- ((F e. CC /\ B e. CC) -> (F x. B) e. CC)
12	11	ad2ant2rl 411	. . . . . . . . . 10 |- (((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC)) -> (F x. B) e. CC)
13		axmulcl 5273	. . . . . . . . . . 11 |- ((A e. CC /\ B e. CC) -> (A x. B) e. CC)
14	13	adantl 388	. . . . . . . . . 10 |- (((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC)) -> (A x. B) e. CC)
15	8, 10, 12, 14	syl3anc 858	. . . . . . . . 9 |- (((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC)) -> (((F x. G) - (F x. B)) + ((F x. B) - (A x. B))) = ((F x. G) - (A x. B)))
16	7, 15	eqtr2d 1508	. . . . . . . 8 |- (((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC)) -> ((F x. G) - (A x. B)) = ((F x. (G - B)) + ((F - A) x. B)))
17	16	fveq2d 3728	. . . . . . 7 |- (((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC)) -> (abs` ((F x. G) - (A x. B))) = (abs` ((F x. (G - B)) + ((F - A) x. B))))
18		abstrit 6898	. . . . . . . 8 |- (((F x. (G - B)) e. CC /\ ((F - A) x. B) e. CC) -> (abs` ((F x. (G - B)) + ((F - A) x. B))) <_ ((abs` (F x. (G - B))) + (abs` ((F - A) x. B))))
19		axmulcl 5273	. . . . . . . . . . 11 |- ((F e. CC /\ (G - B) e. CC) -> (F x. (G - B)) e. CC)
20		subclt 5367	. . . . . . . . . . 11 |- ((G e. CC /\ B e. CC) -> (G - B) e. CC)
21	19, 20	sylan2 451	. . . . . . . . . 10 |- ((F e. CC /\ (G e. CC /\ B e. CC)) -> (F x. (G - B)) e. CC)
22	21	anassrs 441	. . . . . . . . 9 |- (((F e. CC /\ G e. CC) /\ B e. CC) -> (F x. (G - B)) e. CC)
23	22	adantrl 394	. . . . . . . 8 |- (((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC)) -> (F x. (G - B)) e. CC)
24		axmulcl 5273	. . . . . . . . . . 11 |- (((F - A) e. CC /\ B e. CC) -> ((F - A) x. B) e. CC)
25		subclt 5367	. . . . . . . . . . 11 |- ((F e. CC /\ A e. CC) -> (F - A) e. CC)
26	24, 25	sylan 448	. . . . . . . . . 10 |- (((F e. CC /\ A e. CC) /\ B e. CC) -> ((F - A) x. B) e. CC)
27	26	anasss 440	. . . . . . . . 9 |- ((F e. CC /\ (A e. CC /\ B e. CC)) -> ((F - A) x. B) e. CC)
28	27	adantlr 393	. . . . . . . 8 |- (((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC)) -> ((F - A) x. B) e. CC)
29	18, 23, 28	sylanc 471	. . . . . . 7 |- (((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC)) -> (abs` ((F x. (G - B)) + ((F - A) x. B))) <_ ((abs` (F x. (G - B))) + (abs` ((F - A) x. B))))
30	17, 29	eqbrtrd 2635	. . . . . 6 |- (((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC)) -> (abs` ((F x. G) - (A x. B))) <_ ((abs` (F x. (G - B))) + (abs` ((F - A) x. B))))
31	30	3adant3 799	. . . . 5 |- (((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC) /\ (v e. RR /\ 0 < v)) -> (abs` ((F x. G) - (A x. B))) <_ ((abs` (F x. (G - B))) + (abs` ((F - A) x. B))))
32	31	adantr 389	. . . 4 |- ((((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC) /\ (v e. RR /\ 0 < v)) /\ ((abs` (F - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) /\ (abs` (G - B)) < ((v / 2) / (1 + (abs` A))))) -> (abs` ((F x. G) - (A x. B))) <_ ((abs` (F x. (G - B))) + (abs` ((F - A) x. B))))
33		climmullem1 7120	. . . . . . . . . . . 12 |- ((B e. CC /\ (v e. RR /\ 0 < v)) -> (((v / 2) / (1 + (abs` B))) e. RR /\ 0 < ((v / 2) / (1 + (abs` B)))))
34		recrecltt 5902	. . . . . . . . . . . . 13 |- ((((v / 2) / (1 + (abs` B))) e. RR /\ 0 < ((v / 2) / (1 + (abs` B)))) -> ((1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) < 1 /\ (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) < ((v / 2) / (1 + (abs` B)))))
35	34	pm3.26d 321	. . . . . . . . . . . 12 |- ((((v / 2) / (1 + (abs` B))) e. RR /\ 0 < ((v / 2) / (1 + (abs` B)))) -> (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) < 1)
36	33, 35	syl 10	. . . . . . . . . . 11 |- ((B e. CC /\ (v e. RR /\ 0 < v)) -> (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) < 1)
37	36	adantll 392	. . . . . . . . . 10 |- (((A e. CC /\ B e. CC) /\ (v e. RR /\ 0 < v)) -> (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) < 1)
38	37	3adant1 797	. . . . . . . . 9 |- (((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC) /\ (v e. RR /\ 0 < v)) -> (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) < 1)
39		1re 5435	. . . . . . . . . . 11 |- 1 e. RR
40		axlttrn 5504	. . . . . . . . . . 11 |- (((abs` (F - A))