Metamath Proof Explorer


Theorem mbfi1fseqlem3

Description: Lemma for mbfi1fseq . (Contributed by Mario Carneiro, 16-Aug-2014)

Ref Expression
Hypotheses mbfi1fseq.1 φFMblFn
mbfi1fseq.2 φF:0+∞
mbfi1fseq.3 J=m,yFy2m2m
mbfi1fseq.4 G=mxifxmmifmJxmmJxm0
Assertion mbfi1fseqlem3 φAGA:ranm0A2Am2A

Proof

Step Hyp Ref Expression
1 mbfi1fseq.1 φFMblFn
2 mbfi1fseq.2 φF:0+∞
3 mbfi1fseq.3 J=m,yFy2m2m
4 mbfi1fseq.4 G=mxifxmmifmJxmmJxm0
5 1 2 3 4 mbfi1fseqlem2 AGA=xifxAAifAJxAAJxA0
6 5 adantl φAGA=xifxAAifAJxAAJxA0
7 rge0ssre 0+∞
8 simpr myy
9 ffvelcdm F:0+∞yFy0+∞
10 2 8 9 syl2an φmyFy0+∞
11 7 10 sselid φmyFy
12 2nn 2
13 nnnn0 mm0
14 nnexpcl 2m02m
15 12 13 14 sylancr m2m
16 15 ad2antrl φmy2m
17 16 nnred φmy2m
18 11 17 remulcld φmyFy2m
19 reflcl Fy2mFy2m
20 18 19 syl φmyFy2m
21 20 16 nndivred φmyFy2m2m
22 21 ralrimivva φmyFy2m2m
23 3 fmpo myFy2m2mJ:×
24 22 23 sylib φJ:×
25 fovcdm J:×AxAJx
26 24 25 syl3an1 φAxAJx
27 26 3expa φAxAJx
28 nnre AA
29 28 ad2antlr φAxA
30 nnnn0 AA0
31 nnexpcl 2A02A
32 12 30 31 sylancr A2A
33 32 ad2antlr φAx2A
34 nnre 2A2A
35 nngt0 2A0<2A
36 34 35 jca 2A2A0<2A
37 33 36 syl φAx2A0<2A
38 lemul1 AJxA2A0<2AAJxAAJx2AA2A
39 27 29 37 38 syl3anc φAxAJxAAJx2AA2A
40 39 biimpa φAxAJxAAJx2AA2A
41 simpr m=Ay=xy=x
42 41 fveq2d m=Ay=xFy=Fx
43 simpl m=Ay=xm=A
44 43 oveq2d m=Ay=x2m=2A
45 42 44 oveq12d m=Ay=xFy2m=Fx2A
46 45 fveq2d m=Ay=xFy2m=Fx2A
47 46 44 oveq12d m=Ay=xFy2m2m=Fx2A2A
48 ovex Fx2A2AV
49 47 3 48 ovmpoa AxAJx=Fx2A2A
50 49 ad4ant23 φAxAJxAAJx=Fx2A2A
51 50 oveq1d φAxAJxAAJx2A=Fx2A2A2A
52 2 adantr φAF:0+∞
53 52 ffvelcdmda φAxFx0+∞
54 elrege0 Fx0+∞Fx0Fx
55 53 54 sylib φAxFx0Fx
56 55 simpld φAxFx
57 33 nnred φAx2A
58 56 57 remulcld φAxFx2A
59 33 nnnn0d φAx2A0
60 59 nn0ge0d φAx02A
61 mulge0 Fx0Fx2A02A0Fx2A
62 55 57 60 61 syl12anc φAx0Fx2A
63 flge0nn0 Fx2A0Fx2AFx2A0
64 58 62 63 syl2anc φAxFx2A0
65 64 adantr φAxAJxAFx2A0
66 65 nn0cnd φAxAJxAFx2A
67 33 adantr φAxAJxA2A
68 67 nncnd φAxAJxA2A
69 67 nnne0d φAxAJxA2A0
70 66 68 69 divcan1d φAxAJxAFx2A2A2A=Fx2A
71 51 70 eqtrd φAxAJxAAJx2A=Fx2A
72 71 65 eqeltrd φAxAJxAAJx2A0
73 nn0uz 0=0
74 72 73 eleqtrdi φAxAJxAAJx2A0
75 nnmulcl A2AA2A
76 32 75 mpdan AA2A
77 76 ad2antlr φAxA2A
78 77 adantr φAxAJxAA2A
79 78 nnzd φAxAJxAA2A
80 elfz5 AJx2A0A2AAJx2A0A2AAJx2AA2A
81 74 79 80 syl2anc φAxAJxAAJx2A0A2AAJx2AA2A
82 40 81 mpbird φAxAJxAAJx2A0A2A
83 oveq1 m=AJx2Am2A=AJx2A2A
84 eqid m0A2Am2A=m0A2Am2A
85 ovex AJx2A2AV
86 83 84 85 fvmpt AJx2A0A2Am0A2Am2AAJx2A=AJx2A2A
87 82 86 syl φAxAJxAm0A2Am2AAJx2A=AJx2A2A
88 27 adantr φAxAJxAAJx
89 88 recnd φAxAJxAAJx
90 89 68 69 divcan4d φAxAJxAAJx2A2A=AJx
91 87 90 eqtrd φAxAJxAm0A2Am2AAJx2A=AJx
92 elfznn0 m0A2Am0
93 92 nn0red m0A2Am
94 32 adantl φA2A
95 nndivre m2Am2A
96 93 94 95 syl2anr φAm0A2Am2A
97 96 fmpttd φAm0A2Am2A:0A2A
98 97 ffnd φAm0A2Am2AFn0A2A
99 98 adantr φAxm0A2Am2AFn0A2A
100 99 adantr φAxAJxAm0A2Am2AFn0A2A
101 fnfvelrn m0A2Am2AFn0A2AAJx2A0A2Am0A2Am2AAJx2Aranm0A2Am2A
102 100 82 101 syl2anc φAxAJxAm0A2Am2AAJx2Aranm0A2Am2A
103 91 102 eqeltrrd φAxAJxAAJxranm0A2Am2A
104 77 nnnn0d φAxA2A0
105 104 73 eleqtrdi φAxA2A0
106 eluzfz2 A2A0A2A0A2A
107 105 106 syl φAxA2A0A2A
108 oveq1 m=A2Am2A=A2A2A
109 ovex A2A2AV
110 108 84 109 fvmpt A2A0A2Am0A2Am2AA2A=A2A2A
111 107 110 syl φAxm0A2Am2AA2A=A2A2A
112 29 recnd φAxA
113 33 nncnd φAx2A
114 33 nnne0d φAx2A0
115 112 113 114 divcan4d φAxA2A2A=A
116 111 115 eqtrd φAxm0A2Am2AA2A=A
117 fnfvelrn m0A2Am2AFn0A2AA2A0A2Am0A2Am2AA2Aranm0A2Am2A
118 99 107 117 syl2anc φAxm0A2Am2AA2Aranm0A2Am2A
119 116 118 eqeltrrd φAxAranm0A2Am2A
120 119 adantr φAx¬AJxAAranm0A2Am2A
121 103 120 ifclda φAxifAJxAAJxAranm0A2Am2A
122 eluzfz1 A2A000A2A
123 105 122 syl φAx00A2A
124 oveq1 m=0m2A=02A
125 ovex 02AV
126 124 84 125 fvmpt 00A2Am0A2Am2A0=02A
127 123 126 syl φAxm0A2Am2A0=02A
128 nncn 2A2A
129 nnne0 2A2A0
130 128 129 div0d 2A02A=0
131 33 130 syl φAx02A=0
132 127 131 eqtrd φAxm0A2Am2A0=0
133 fnfvelrn m0A2Am2AFn0A2A00A2Am0A2Am2A0ranm0A2Am2A
134 99 123 133 syl2anc φAxm0A2Am2A0ranm0A2Am2A
135 132 134 eqeltrrd φAx0ranm0A2Am2A
136 121 135 ifcld φAxifxAAifAJxAAJxA0ranm0A2Am2A
137 6 136 fmpt3d φAGA:ranm0A2Am2A