Metamath Proof Explorer

Theorem eirrlem

Description: Lemma for eirr . (Contributed by Paul Chapman, 9-Feb-2008) (Revised by Mario Carneiro, 29-Apr-2014)

Ref Expression
Hypotheses eirr.1 
|- F = ( n e. NN0 |-> ( 1 / ( ! ` n ) ) )
eirr.2 
|- ( ph -> P e. ZZ )
eirr.3 
|- ( ph -> Q e. NN )
eirr.4 
|- ( ph -> _e = ( P / Q ) )
Assertion eirrlem 
|- -. ph

Proof

Step Hyp Ref Expression
1 eirr.1 
 |-  F = ( n e. NN0 |-> ( 1 / ( ! ` n ) ) )
2 eirr.2 
 |-  ( ph -> P e. ZZ )
3 eirr.3 
 |-  ( ph -> Q e. NN )
4 eirr.4 
 |-  ( ph -> _e = ( P / Q ) )
5 fzfid 
 |-  ( ph -> ( 0 ... Q ) e. Fin )
6 elfznn0 
 |-  ( k e. ( 0 ... Q ) -> k e. NN0 )
7 nn0z 
 |-  ( n e. NN0 -> n e. ZZ )
8 1exp 
 |-  ( n e. ZZ -> ( 1 ^ n ) = 1 )
9 7 8 syl 
 |-  ( n e. NN0 -> ( 1 ^ n ) = 1 )
10 9 oveq1d 
 |-  ( n e. NN0 -> ( ( 1 ^ n ) / ( ! ` n ) ) = ( 1 / ( ! ` n ) ) )
11 10 mpteq2ia 
 |-  ( n e. NN0 |-> ( ( 1 ^ n ) / ( ! ` n ) ) ) = ( n e. NN0 |-> ( 1 / ( ! ` n ) ) )
12 1 11 eqtr4i 
 |-  F = ( n e. NN0 |-> ( ( 1 ^ n ) / ( ! ` n ) ) )
13 12 eftval 
 |-  ( k e. NN0 -> ( F ` k ) = ( ( 1 ^ k ) / ( ! ` k ) ) )
14 13 adantl 
 |-  ( ( ph /\ k e. NN0 ) -> ( F ` k ) = ( ( 1 ^ k ) / ( ! ` k ) ) )
15 ax-1cn 
 |-  1 e. CC
16 15 a1i 
 |-  ( ph -> 1 e. CC )
17 eftcl 
 |-  ( ( 1 e. CC /\ k e. NN0 ) -> ( ( 1 ^ k ) / ( ! ` k ) ) e. CC )
18 16 17 sylan 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( 1 ^ k ) / ( ! ` k ) ) e. CC )
19 14 18 eqeltrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( F ` k ) e. CC )
20 6 19 sylan2 
 |-  ( ( ph /\ k e. ( 0 ... Q ) ) -> ( F ` k ) e. CC )
21 5 20 fsumcl 
 |-  ( ph -> sum_ k e. ( 0 ... Q ) ( F ` k ) e. CC )
22 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
23 eqid 
 |-  ( ZZ>= ` ( Q + 1 ) ) = ( ZZ>= ` ( Q + 1 ) )
24 3 peano2nnd 
 |-  ( ph -> ( Q + 1 ) e. NN )
25 24 nnnn0d 
 |-  ( ph -> ( Q + 1 ) e. NN0 )
26 eqidd 
 |-  ( ( ph /\ k e. NN0 ) -> ( F ` k ) = ( F ` k ) )
27 fveq2 
 |-  ( n = k -> ( ! ` n ) = ( ! ` k ) )
28 27 oveq2d 
 |-  ( n = k -> ( 1 / ( ! ` n ) ) = ( 1 / ( ! ` k ) ) )
29 ovex 
 |-  ( 1 / ( ! ` k ) ) e. _V
30 28 1 29 fvmpt 
 |-  ( k e. NN0 -> ( F ` k ) = ( 1 / ( ! ` k ) ) )
31 30 adantl 
 |-  ( ( ph /\ k e. NN0 ) -> ( F ` k ) = ( 1 / ( ! ` k ) ) )
32 faccl 
 |-  ( k e. NN0 -> ( ! ` k ) e. NN )
33 32 adantl 
 |-  ( ( ph /\ k e. NN0 ) -> ( ! ` k ) e. NN )
34 33 nnrpd 
 |-  ( ( ph /\ k e. NN0 ) -> ( ! ` k ) e. RR+ )
35 34 rpreccld 
 |-  ( ( ph /\ k e. NN0 ) -> ( 1 / ( ! ` k ) ) e. RR+ )
36 31 35 eqeltrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( F ` k ) e. RR+ )
37 12 efcllem 
 |-  ( 1 e. CC -> seq 0 ( + , F ) e. dom ~~> )
38 16 37 syl 
 |-  ( ph -> seq 0 ( + , F ) e. dom ~~> )
39 22 23 25 26 36 38 isumrpcl 
 |-  ( ph -> sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) e. RR+ )
40 39 rpred 
 |-  ( ph -> sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) e. RR )
41 40 recnd 
 |-  ( ph -> sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) e. CC )
42 esum 
 |-  _e = sum_ k e. NN0 ( 1 / ( ! ` k ) )
43 30 sumeq2i 
 |-  sum_ k e. NN0 ( F ` k ) = sum_ k e. NN0 ( 1 / ( ! ` k ) )
44 42 43 eqtr4i 
 |-  _e = sum_ k e. NN0 ( F ` k )
45 22 23 25 26 19 38 isumsplit 
 |-  ( ph -> sum_ k e. NN0 ( F ` k ) = ( sum_ k e. ( 0 ... ( ( Q + 1 ) - 1 ) ) ( F ` k ) + sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) )
46 44 45 eqtrid 
 |-  ( ph -> _e = ( sum_ k e. ( 0 ... ( ( Q + 1 ) - 1 ) ) ( F ` k ) + sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) )
47 3 nncnd 
 |-  ( ph -> Q e. CC )
48 pncan 
 |-  ( ( Q e. CC /\ 1 e. CC ) -> ( ( Q + 1 ) - 1 ) = Q )
49 47 15 48 sylancl 
 |-  ( ph -> ( ( Q + 1 ) - 1 ) = Q )
50 49 oveq2d 
 |-  ( ph -> ( 0 ... ( ( Q + 1 ) - 1 ) ) = ( 0 ... Q ) )
51 50 sumeq1d 
 |-  ( ph -> sum_ k e. ( 0 ... ( ( Q + 1 ) - 1 ) ) ( F ` k ) = sum_ k e. ( 0 ... Q ) ( F ` k ) )
52 51 oveq1d 
 |-  ( ph -> ( sum_ k e. ( 0 ... ( ( Q + 1 ) - 1 ) ) ( F ` k ) + sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) = ( sum_ k e. ( 0 ... Q ) ( F ` k ) + sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) )
53 46 52 eqtrd 
 |-  ( ph -> _e = ( sum_ k e. ( 0 ... Q ) ( F ` k ) + sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) )
54 21 41 53 mvrladdd 
 |-  ( ph -> ( _e - sum_ k e. ( 0 ... Q ) ( F ` k ) ) = sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) )
55 54 oveq2d 
 |-  ( ph -> ( ( ! ` Q ) x. ( _e - sum_ k e. ( 0 ... Q ) ( F ` k ) ) ) = ( ( ! ` Q ) x. sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) )
56 3 nnnn0d 
 |-  ( ph -> Q e. NN0 )
57 56 faccld 
 |-  ( ph -> ( ! ` Q ) e. NN )
58 57 nncnd 
 |-  ( ph -> ( ! ` Q ) e. CC )
59 ere 
 |-  _e e. RR
60 59 recni 
 |-  _e e. CC
61 60 a1i 
 |-  ( ph -> _e e. CC )
62 58 61 21 subdid 
 |-  ( ph -> ( ( ! ` Q ) x. ( _e - sum_ k e. ( 0 ... Q ) ( F ` k ) ) ) = ( ( ( ! ` Q ) x. _e ) - ( ( ! ` Q ) x. sum_ k e. ( 0 ... Q ) ( F ` k ) ) ) )
63 55 62 eqtr3d 
 |-  ( ph -> ( ( ! ` Q ) x. sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) = ( ( ( ! ` Q ) x. _e ) - ( ( ! ` Q ) x. sum_ k e. ( 0 ... Q ) ( F ` k ) ) ) )
64 4 oveq2d 
 |-  ( ph -> ( ( ! ` Q ) x. _e ) = ( ( ! ` Q ) x. ( P / Q ) ) )
65 2 zcnd 
 |-  ( ph -> P e. CC )
66 3 nnne0d 
 |-  ( ph -> Q =/= 0 )
67 58 65 47 66 div12d 
 |-  ( ph -> ( ( ! ` Q ) x. ( P / Q ) ) = ( P x. ( ( ! ` Q ) / Q ) ) )
68 64 67 eqtrd 
 |-  ( ph -> ( ( ! ` Q ) x. _e ) = ( P x. ( ( ! ` Q ) / Q ) ) )
69 3 nnred 
 |-  ( ph -> Q e. RR )
70 69 leidd 
 |-  ( ph -> Q <_ Q )
71 facdiv 
 |-  ( ( Q e. NN0 /\ Q e. NN /\ Q <_ Q ) -> ( ( ! ` Q ) / Q ) e. NN )
72 56 3 70 71 syl3anc 
 |-  ( ph -> ( ( ! ` Q ) / Q ) e. NN )
73 72 nnzd 
 |-  ( ph -> ( ( ! ` Q ) / Q ) e. ZZ )
74 2 73 zmulcld 
 |-  ( ph -> ( P x. ( ( ! ` Q ) / Q ) ) e. ZZ )
75 68 74 eqeltrd 
 |-  ( ph -> ( ( ! ` Q ) x. _e ) e. ZZ )
76 5 58 20 fsummulc2 
 |-  ( ph -> ( ( ! ` Q ) x. sum_ k e. ( 0 ... Q ) ( F ` k ) ) = sum_ k e. ( 0 ... Q ) ( ( ! ` Q ) x. ( F ` k ) ) )
77 6 adantl 
 |-  ( ( ph /\ k e. ( 0 ... Q ) ) -> k e. NN0 )
78 77 30 syl 
 |-  ( ( ph /\ k e. ( 0 ... Q ) ) -> ( F ` k ) = ( 1 / ( ! ` k ) ) )
79 78 oveq2d 
 |-  ( ( ph /\ k e. ( 0 ... Q ) ) -> ( ( ! ` Q ) x. ( F ` k ) ) = ( ( ! ` Q ) x. ( 1 / ( ! ` k ) ) ) )
80 58 adantr 
 |-  ( ( ph /\ k e. ( 0 ... Q ) ) -> ( ! ` Q ) e. CC )
81 6 33 sylan2 
 |-  ( ( ph /\ k e. ( 0 ... Q ) ) -> ( ! ` k ) e. NN )
82 81 nncnd 
 |-  ( ( ph /\ k e. ( 0 ... Q ) ) -> ( ! ` k ) e. CC )
83 facne0 
 |-  ( k e. NN0 -> ( ! ` k ) =/= 0 )
84 77 83 syl 
 |-  ( ( ph /\ k e. ( 0 ... Q ) ) -> ( ! ` k ) =/= 0 )
85 80 82 84 divrecd 
 |-  ( ( ph /\ k e. ( 0 ... Q ) ) -> ( ( ! ` Q ) / ( ! ` k ) ) = ( ( ! ` Q ) x. ( 1 / ( ! ` k ) ) ) )
86 79 85 eqtr4d 
 |-  ( ( ph /\ k e. ( 0 ... Q ) ) -> ( ( ! ` Q ) x. ( F ` k ) ) = ( ( ! ` Q ) / ( ! ` k ) ) )
87 permnn 
 |-  ( k e. ( 0 ... Q ) -> ( ( ! ` Q ) / ( ! ` k ) ) e. NN )
88 87 adantl 
 |-  ( ( ph /\ k e. ( 0 ... Q ) ) -> ( ( ! ` Q ) / ( ! ` k ) ) e. NN )
89 86 88 eqeltrd 
 |-  ( ( ph /\ k e. ( 0 ... Q ) ) -> ( ( ! ` Q ) x. ( F ` k ) ) e. NN )
90 89 nnzd 
 |-  ( ( ph /\ k e. ( 0 ... Q ) ) -> ( ( ! ` Q ) x. ( F ` k ) ) e. ZZ )
91 5 90 fsumzcl 
 |-  ( ph -> sum_ k e. ( 0 ... Q ) ( ( ! ` Q ) x. ( F ` k ) ) e. ZZ )
92 76 91 eqeltrd 
 |-  ( ph -> ( ( ! ` Q ) x. sum_ k e. ( 0 ... Q ) ( F ` k ) ) e. ZZ )
93 75 92 zsubcld 
 |-  ( ph -> ( ( ( ! ` Q ) x. _e ) - ( ( ! ` Q ) x. sum_ k e. ( 0 ... Q ) ( F ` k ) ) ) e. ZZ )
94 63 93 eqeltrd 
 |-  ( ph -> ( ( ! ` Q ) x. sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) e. ZZ )
95 0zd 
 |-  ( ph -> 0 e. ZZ )
96 57 nnrpd 
 |-  ( ph -> ( ! ` Q ) e. RR+ )
97 96 39 rpmulcld 
 |-  ( ph -> ( ( ! ` Q ) x. sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) e. RR+ )
98 97 rpgt0d 
 |-  ( ph -> 0 < ( ( ! ` Q ) x. sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) )
99 24 peano2nnd 
 |-  ( ph -> ( ( Q + 1 ) + 1 ) e. NN )
100 99 nnred 
 |-  ( ph -> ( ( Q + 1 ) + 1 ) e. RR )
101 25 faccld 
 |-  ( ph -> ( ! ` ( Q + 1 ) ) e. NN )
102 101 24 nnmulcld 
 |-  ( ph -> ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) e. NN )
103 100 102 nndivred 
 |-  ( ph -> ( ( ( Q + 1 ) + 1 ) / ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) ) e. RR )
104 57 nnrecred 
 |-  ( ph -> ( 1 / ( ! ` Q ) ) e. RR )
105 abs1 
 |-  ( abs ` 1 ) = 1
106 105 oveq1i 
 |-  ( ( abs ` 1 ) ^ n ) = ( 1 ^ n )
107 106 oveq1i 
 |-  ( ( ( abs ` 1 ) ^ n ) / ( ! ` n ) ) = ( ( 1 ^ n ) / ( ! ` n ) )
108 107 mpteq2i 
 |-  ( n e. NN0 |-> ( ( ( abs ` 1 ) ^ n ) / ( ! ` n ) ) ) = ( n e. NN0 |-> ( ( 1 ^ n ) / ( ! ` n ) ) )
109 12 108 eqtr4i 
 |-  F = ( n e. NN0 |-> ( ( ( abs ` 1 ) ^ n ) / ( ! ` n ) ) )
110 eqid 
 |-  ( n e. NN0 |-> ( ( ( ( abs ` 1 ) ^ ( Q + 1 ) ) / ( ! ` ( Q + 1 ) ) ) x. ( ( 1 / ( ( Q + 1 ) + 1 ) ) ^ n ) ) ) = ( n e. NN0 |-> ( ( ( ( abs ` 1 ) ^ ( Q + 1 ) ) / ( ! ` ( Q + 1 ) ) ) x. ( ( 1 / ( ( Q + 1 ) + 1 ) ) ^ n ) ) )
111 1le1 
 |-  1 <_ 1
112 105 111 eqbrtri 
 |-  ( abs ` 1 ) <_ 1
113 112 a1i 
 |-  ( ph -> ( abs ` 1 ) <_ 1 )
114 12 109 110 24 16 113 eftlub 
 |-  ( ph -> ( abs ` sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) <_ ( ( ( abs ` 1 ) ^ ( Q + 1 ) ) x. ( ( ( Q + 1 ) + 1 ) / ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) ) ) )
115 39 rprege0d 
 |-  ( ph -> ( sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) e. RR /\ 0 <_ sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) )
116 absid 
 |-  ( ( sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) e. RR /\ 0 <_ sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) -> ( abs ` sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) = sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) )
117 115 116 syl 
 |-  ( ph -> ( abs ` sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) = sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) )
118 105 oveq1i 
 |-  ( ( abs ` 1 ) ^ ( Q + 1 ) ) = ( 1 ^ ( Q + 1 ) )
119 24 nnzd 
 |-  ( ph -> ( Q + 1 ) e. ZZ )
120 1exp 
 |-  ( ( Q + 1 ) e. ZZ -> ( 1 ^ ( Q + 1 ) ) = 1 )
121 119 120 syl 
 |-  ( ph -> ( 1 ^ ( Q + 1 ) ) = 1 )
122 118 121 eqtrid 
 |-  ( ph -> ( ( abs ` 1 ) ^ ( Q + 1 ) ) = 1 )
123 122 oveq1d 
 |-  ( ph -> ( ( ( abs ` 1 ) ^ ( Q + 1 ) ) x. ( ( ( Q + 1 ) + 1 ) / ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) ) ) = ( 1 x. ( ( ( Q + 1 ) + 1 ) / ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) ) ) )
124 103 recnd 
 |-  ( ph -> ( ( ( Q + 1 ) + 1 ) / ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) ) e. CC )
125 124 mullidd 
 |-  ( ph -> ( 1 x. ( ( ( Q + 1 ) + 1 ) / ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) ) ) = ( ( ( Q + 1 ) + 1 ) / ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) ) )
126 123 125 eqtrd 
 |-  ( ph -> ( ( ( abs ` 1 ) ^ ( Q + 1 ) ) x. ( ( ( Q + 1 ) + 1 ) / ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) ) ) = ( ( ( Q + 1 ) + 1 ) / ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) ) )
127 114 117 126 3brtr3d 
 |-  ( ph -> sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) <_ ( ( ( Q + 1 ) + 1 ) / ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) ) )
128 24 nnred 
 |-  ( ph -> ( Q + 1 ) e. RR )
129 128 128 readdcld 
 |-  ( ph -> ( ( Q + 1 ) + ( Q + 1 ) ) e. RR )
130 128 128 remulcld 
 |-  ( ph -> ( ( Q + 1 ) x. ( Q + 1 ) ) e. RR )
131 1red 
 |-  ( ph -> 1 e. RR )
132 3 nnge1d 
 |-  ( ph -> 1 <_ Q )
133 1nn 
 |-  1 e. NN
134 nnleltp1 
 |-  ( ( 1 e. NN /\ Q e. NN ) -> ( 1 <_ Q <-> 1 < ( Q + 1 ) ) )
135 133 3 134 sylancr 
 |-  ( ph -> ( 1 <_ Q <-> 1 < ( Q + 1 ) ) )
136 132 135 mpbid 
 |-  ( ph -> 1 < ( Q + 1 ) )
137 131 128 128 136 ltadd2dd 
 |-  ( ph -> ( ( Q + 1 ) + 1 ) < ( ( Q + 1 ) + ( Q + 1 ) ) )
138 24 nncnd 
 |-  ( ph -> ( Q + 1 ) e. CC )
139 138 2timesd 
 |-  ( ph -> ( 2 x. ( Q + 1 ) ) = ( ( Q + 1 ) + ( Q + 1 ) ) )
140 df-2 
 |-  2 = ( 1 + 1 )
141 131 69 131 132 leadd1dd 
 |-  ( ph -> ( 1 + 1 ) <_ ( Q + 1 ) )
142 140 141 eqbrtrid 
 |-  ( ph -> 2 <_ ( Q + 1 ) )
143 2re 
 |-  2 e. RR
144 143 a1i 
 |-  ( ph -> 2 e. RR )
145 24 nngt0d 
 |-  ( ph -> 0 < ( Q + 1 ) )
146 lemul1 
 |-  ( ( 2 e. RR /\ ( Q + 1 ) e. RR /\ ( ( Q + 1 ) e. RR /\ 0 < ( Q + 1 ) ) ) -> ( 2 <_ ( Q + 1 ) <-> ( 2 x. ( Q + 1 ) ) <_ ( ( Q + 1 ) x. ( Q + 1 ) ) ) )
147 144 128 128 145 146 syl112anc 
 |-  ( ph -> ( 2 <_ ( Q + 1 ) <-> ( 2 x. ( Q + 1 ) ) <_ ( ( Q + 1 ) x. ( Q + 1 ) ) ) )
148 142 147 mpbid 
 |-  ( ph -> ( 2 x. ( Q + 1 ) ) <_ ( ( Q + 1 ) x. ( Q + 1 ) ) )
149 139 148 eqbrtrrd 
 |-  ( ph -> ( ( Q + 1 ) + ( Q + 1 ) ) <_ ( ( Q + 1 ) x. ( Q + 1 ) ) )
150 100 129 130 137 149 ltletrd 
 |-  ( ph -> ( ( Q + 1 ) + 1 ) < ( ( Q + 1 ) x. ( Q + 1 ) ) )
151 facp1 
 |-  ( Q e. NN0 -> ( ! ` ( Q + 1 ) ) = ( ( ! ` Q ) x. ( Q + 1 ) ) )
152 56 151 syl 
 |-  ( ph -> ( ! ` ( Q + 1 ) ) = ( ( ! ` Q ) x. ( Q + 1 ) ) )
153 152 oveq1d 
 |-  ( ph -> ( ( ! ` ( Q + 1 ) ) / ( ! ` Q ) ) = ( ( ( ! ` Q ) x. ( Q + 1 ) ) / ( ! ` Q ) ) )
154 101 nncnd 
 |-  ( ph -> ( ! ` ( Q + 1 ) ) e. CC )
155 57 nnne0d 
 |-  ( ph -> ( ! ` Q ) =/= 0 )
156 154 58 155 divrecd 
 |-  ( ph -> ( ( ! ` ( Q + 1 ) ) / ( ! ` Q ) ) = ( ( ! ` ( Q + 1 ) ) x. ( 1 / ( ! ` Q ) ) ) )
157 138 58 155 divcan3d 
 |-  ( ph -> ( ( ( ! ` Q ) x. ( Q + 1 ) ) / ( ! ` Q ) ) = ( Q + 1 ) )
158 153 156 157 3eqtr3rd 
 |-  ( ph -> ( Q + 1 ) = ( ( ! ` ( Q + 1 ) ) x. ( 1 / ( ! ` Q ) ) ) )
159 158 oveq1d 
 |-  ( ph -> ( ( Q + 1 ) x. ( Q + 1 ) ) = ( ( ( ! ` ( Q + 1 ) ) x. ( 1 / ( ! ` Q ) ) ) x. ( Q + 1 ) ) )
160 104 recnd 
 |-  ( ph -> ( 1 / ( ! ` Q ) ) e. CC )
161 154 160 138 mul32d 
 |-  ( ph -> ( ( ( ! ` ( Q + 1 ) ) x. ( 1 / ( ! ` Q ) ) ) x. ( Q + 1 ) ) = ( ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) x. ( 1 / ( ! ` Q ) ) ) )
162 159 161 eqtrd 
 |-  ( ph -> ( ( Q + 1 ) x. ( Q + 1 ) ) = ( ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) x. ( 1 / ( ! ` Q ) ) ) )
163 150 162 breqtrd 
 |-  ( ph -> ( ( Q + 1 ) + 1 ) < ( ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) x. ( 1 / ( ! ` Q ) ) ) )
164 102 nnred 
 |-  ( ph -> ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) e. RR )
165 102 nngt0d 
 |-  ( ph -> 0 < ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) )
166 ltdivmul 
 |-  ( ( ( ( Q + 1 ) + 1 ) e. RR /\ ( 1 / ( ! ` Q ) ) e. RR /\ ( ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) e. RR /\ 0 < ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) ) ) -> ( ( ( ( Q + 1 ) + 1 ) / ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) ) < ( 1 / ( ! ` Q ) ) <-> ( ( Q + 1 ) + 1 ) < ( ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) x. ( 1 / ( ! ` Q ) ) ) ) )
167 100 104 164 165 166 syl112anc 
 |-  ( ph -> ( ( ( ( Q + 1 ) + 1 ) / ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) ) < ( 1 / ( ! ` Q ) ) <-> ( ( Q + 1 ) + 1 ) < ( ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) x. ( 1 / ( ! ` Q ) ) ) ) )
168 163 167 mpbird 
 |-  ( ph -> ( ( ( Q + 1 ) + 1 ) / ( ( ! ` ( Q + 1 ) ) x. ( Q + 1 ) ) ) < ( 1 / ( ! ` Q ) ) )
169 40 103 104 127 168 lelttrd 
 |-  ( ph -> sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) < ( 1 / ( ! ` Q ) ) )
170 40 131 96 ltmuldiv2d 
 |-  ( ph -> ( ( ( ! ` Q ) x. sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) < 1 <-> sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) < ( 1 / ( ! ` Q ) ) ) )
171 169 170 mpbird 
 |-  ( ph -> ( ( ! ` Q ) x. sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) < 1 )
172 0p1e1 
 |-  ( 0 + 1 ) = 1
173 171 172 breqtrrdi 
 |-  ( ph -> ( ( ! ` Q ) x. sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) < ( 0 + 1 ) )
174 btwnnz 
 |-  ( ( 0 e. ZZ /\ 0 < ( ( ! ` Q ) x. sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) /\ ( ( ! ` Q ) x. sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) < ( 0 + 1 ) ) -> -. ( ( ! ` Q ) x. sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) e. ZZ )
175 95 98 173 174 syl3anc 
 |-  ( ph -> -. ( ( ! ` Q ) x. sum_ k e. ( ZZ>= ` ( Q + 1 ) ) ( F ` k ) ) e. ZZ )
176 94 175 pm2.65i 
 |-  -. ph