Theorem climmullem8 7127

Description: Lemma for climmul 7128. Warning: The HTML proof page is 3/4 megabyte in size.

Hypotheses

Ref	Expression
climmul.1	|- F e. V
climmul.2	|- G e. V
climmul.3	|- H e. V
climmul.4	|- A e. V
climmul.5	|- B e. V
climmullem.6	|- (ph <-> ((F ~~> A /\ G ~~> B) /\ A.k e. (ZZ>` M)((F` k) e. CC /\ (G` k) e. CC /\ (H` k) = ((F` k) x. (G` k)))))

Assertion

Ref	Expression
climmullem8	|- ((M e. ZZ /\ ph) -> H ~~> (A x. B))

Distinct variable groups:   k,F   k,G   k,H   k,M

Proof of Theorem climmullem8

Step	Hyp	Ref	Expression
1		climmullem2 7121	. . . . . . . . 9 |- ((B e. CC /\ (v e. RR /\ 0 < v)) -> ((1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) e. RR /\ 0 < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B))))))))
2		climmul.1	. . . . . . . . . . 11 |- F e. V
3		climmul.2	. . . . . . . . . . 11 |- G e. V
4		climmul.3	. . . . . . . . . . 11 |- H e. V
5		climmul.4	. . . . . . . . . . 11 |- A e. V
6		climmul.5	. . . . . . . . . . 11 |- B e. V
7		climmullem.6	. . . . . . . . . . 11 |- (ph <-> ((F ~~> A /\ G ~~> B) /\ A.k e. (ZZ>` M)((F` k) e. CC /\ (G` k) e. CC /\ (H` k) = ((F` k) x. (G` k)))))
8	2, 3, 4, 5, 6, 7	climmullem7 7126	. . . . . . . . . 10 |- (ph -> (A e. CC /\ B e. CC))
9	8	pm3.27d 325	. . . . . . . . 9 |- (ph -> B e. CC)
10	1, 9	sylan 448	. . . . . . . 8 |- ((ph /\ (v e. RR /\ 0 < v)) -> ((1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) e. RR /\ 0 < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B))))))))
11		climmullem1 7120	. . . . . . . . 9 |- ((A e. CC /\ (v e. RR /\ 0 < v)) -> (((v / 2) / (1 + (abs` A))) e. RR /\ 0 < ((v / 2) / (1 + (abs` A)))))
12	8	pm3.26d 321	. . . . . . . . 9 |- (ph -> A e. CC)
13	11, 12	sylan 448	. . . . . . . 8 |- ((ph /\ (v e. RR /\ 0 < v)) -> (((v / 2) / (1 + (abs` A))) e. RR /\ 0 < ((v / 2) / (1 + (abs` A)))))
14	10, 13	jca 288	. . . . . . 7 |- ((ph /\ (v e. RR /\ 0 < v)) -> (((1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) e. RR /\ 0 < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B))))))) /\ (((v / 2) / (1 + (abs` A))) e. RR /\ 0 < ((v / 2) / (1 + (abs` A))))))
15		0z 6146	. . . . . . . . . . . . 13 |- 0 e. ZZ
16		ssid 2080	. . . . . . . . . . . . 13 |- (ZZ>` 0) (_ (ZZ>` 0)
17		uzssz 6430	. . . . . . . . . . . . 13 |- (ZZ>` M) (_ ZZ
18	15, 16, 17	clmi2 7087	. . . . . . . . . . . 12 |- (((A e. V /\ F ~~> A) /\ ((1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) e. RR /\ 0 < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))))) -> E.u e. (ZZ>` 0)A.t e. (ZZ>` M)(u <_ t -> (abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B))))))))
19	5, 18	mpanl1 706	. . . . . . . . . . 11 |- ((F ~~> A /\ ((1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) e. RR /\ 0 < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))))) -> E.u e. (ZZ>` 0)A.t e. (ZZ>` M)(u <_ t -> (abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B))))))))
20	15, 16, 17	clmi2 7087	. . . . . . . . . . . 12 |- (((B e. V /\ G ~~> B) /\ (((v / 2) / (1 + (abs` A))) e. RR /\ 0 < ((v / 2) / (1 + (abs` A))))) -> E.f e. (ZZ>` 0)A.g e. (ZZ>` M)(f <_ g -> (abs` ((G` g) - B)) < ((v / 2) / (1 + (abs` A)))))
21	6, 20	mpanl1 706	. . . . . . . . . . 11 |- ((G ~~> B /\ (((v / 2) / (1 + (abs` A))) e. RR /\ 0 < ((v / 2) / (1 + (abs` A))))) -> E.f e. (ZZ>` 0)A.g e. (ZZ>` M)(f <_ g -> (abs` ((G` g) - B)) < ((v / 2) / (1 + (abs` A)))))
22	19, 21	anim12i 333	. . . . . . . . . 10 |- (((F ~~> A /\ ((1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) e. RR /\ 0 < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))))) /\ (G ~~> B /\ (((v / 2) / (1 + (abs` A))) e. RR /\ 0 < ((v / 2) / (1 + (abs` A)))))) -> (E.u e. (ZZ>` 0)A.t e. (ZZ>` M)(u <_ t -> (abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B))))))) /\ E.f e. (ZZ>` 0)A.g e. (ZZ>` M)(f <_ g -> (abs` ((G` g) - B)) < ((v / 2) / (1 + (abs` A))))))
23	22	an4s 508	. . . . . . . . 9 |- (((F ~~> A /\ G ~~> B) /\ (((1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) e. RR /\ 0 < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B))))))) /\ (((v / 2) / (1 + (abs` A))) e. RR /\ 0 < ((v / 2) / (1 + (abs` A)))))) -> (E.u e. (ZZ>` 0)A.t e. (ZZ>` M)(u <_ t -> (abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B))))))) /\ E.f e. (ZZ>` 0)A.g e. (ZZ>` M)(f <_ g -> (abs` ((G` g) - B)) < ((v / 2) / (1 + (abs` A))))))
24	23	adantlr 393	. . . . . . . 8 |- ((((F ~~> A /\ G ~~> B) /\ A.k e. (ZZ>` M)((F` k) e. CC /\ (G` k) e. CC /\ (H` k) = ((F` k) x. (G` k)))) /\ (((1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) e. RR /\ 0 < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B))))))) /\ (((v / 2) / (1 + (abs` A))) e. RR /\ 0 < ((v / 2) / (1 + (abs` A)))))) -> (E.u e. (ZZ>` 0)A.t e. (ZZ>` M)(u <_ t -> (abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B))))))) /\ E.f e. (ZZ>` 0)A.g e. (ZZ>` M)(f <_ g -> (abs` ((G` g) - B)) < ((v / 2) / (1 + (abs` A))))))
25	24, 7	sylanb 449	. . . . . . 7 |- ((ph /\ (((1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) e. RR /\ 0 < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B))))))) /\ (((v / 2) / (1 + (abs` A))) e. RR /\ 0 < ((v / 2) / (1 + (abs` A)))))) -> (E.u e. (ZZ>` 0)A.t e. (ZZ>` M)(u <_ t -> (abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B))))))) /\ E.f e. (ZZ>` 0)A.g e. (ZZ>` M)(f <_ g -> (abs` ((G` g) - B)) < ((v / 2) / (1 + (abs` A)))))