Metamath Proof Explorer

Theorem prmreclem6

Description: Lemma for prmrec . If the series F was convergent, there would be some k such that the sum starting from k + 1 sums to less than 1 / 2 ; this is a sufficient hypothesis for prmreclem5 to produce the contradictory bound N / 2 < ( 2 ^ k ) sqrt N , which is false for N = 2 ^ ( 2 k + 2 ) . (Contributed by Mario Carneiro, 6-Aug-2014)

Ref Expression
Hypothesis prmrec.1 
|- F = ( n e. NN |-> if ( n e. Prime , ( 1 / n ) , 0 ) )
Assertion prmreclem6 
|- -. seq 1 ( + , F ) e. dom ~~>

Proof

Step Hyp Ref Expression
1 prmrec.1 
 |-  F = ( n e. NN |-> if ( n e. Prime , ( 1 / n ) , 0 ) )
2 nnuz 
 |-  NN = ( ZZ>= ` 1 )
3 1zzd 
 |-  ( T. -> 1 e. ZZ )
4 nnrecre 
 |-  ( n e. NN -> ( 1 / n ) e. RR )
5 4 adantl 
 |-  ( ( T. /\ n e. NN ) -> ( 1 / n ) e. RR )
6 0re 
 |-  0 e. RR
7 ifcl 
 |-  ( ( ( 1 / n ) e. RR /\ 0 e. RR ) -> if ( n e. Prime , ( 1 / n ) , 0 ) e. RR )
8 5 6 7 sylancl 
 |-  ( ( T. /\ n e. NN ) -> if ( n e. Prime , ( 1 / n ) , 0 ) e. RR )
9 8 1 fmptd 
 |-  ( T. -> F : NN --> RR )
10 9 ffvelcdmda 
 |-  ( ( T. /\ j e. NN ) -> ( F ` j ) e. RR )
11 2 3 10 serfre 
 |-  ( T. -> seq 1 ( + , F ) : NN --> RR )
12 11 mptru 
 |-  seq 1 ( + , F ) : NN --> RR
13 frn 
 |-  ( seq 1 ( + , F ) : NN --> RR -> ran seq 1 ( + , F ) C_ RR )
14 12 13 mp1i 
 |-  ( seq 1 ( + , F ) e. dom ~~> -> ran seq 1 ( + , F ) C_ RR )
15 1nn 
 |-  1 e. NN
16 12 fdmi 
 |-  dom seq 1 ( + , F ) = NN
17 15 16 eleqtrri 
 |-  1 e. dom seq 1 ( + , F )
18 ne0i 
 |-  ( 1 e. dom seq 1 ( + , F ) -> dom seq 1 ( + , F ) =/= (/) )
19 dm0rn0 
 |-  ( dom seq 1 ( + , F ) = (/) <-> ran seq 1 ( + , F ) = (/) )
20 19 necon3bii 
 |-  ( dom seq 1 ( + , F ) =/= (/) <-> ran seq 1 ( + , F ) =/= (/) )
21 18 20 sylib 
 |-  ( 1 e. dom seq 1 ( + , F ) -> ran seq 1 ( + , F ) =/= (/) )
22 17 21 mp1i 
 |-  ( seq 1 ( + , F ) e. dom ~~> -> ran seq 1 ( + , F ) =/= (/) )
23 1zzd 
 |-  ( seq 1 ( + , F ) e. dom ~~> -> 1 e. ZZ )
24 climdm 
 |-  ( seq 1 ( + , F ) e. dom ~~> <-> seq 1 ( + , F ) ~~> ( ~~> ` seq 1 ( + , F ) ) )
25 24 biimpi 
 |-  ( seq 1 ( + , F ) e. dom ~~> -> seq 1 ( + , F ) ~~> ( ~~> ` seq 1 ( + , F ) ) )
26 12 a1i 
 |-  ( seq 1 ( + , F ) e. dom ~~> -> seq 1 ( + , F ) : NN --> RR )
27 26 ffvelcdmda 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( seq 1 ( + , F ) ` k ) e. RR )
28 2 23 25 27 climrecl 
 |-  ( seq 1 ( + , F ) e. dom ~~> -> ( ~~> ` seq 1 ( + , F ) ) e. RR )
29 simpr 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> k e. NN )
30 25 adantr 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> seq 1 ( + , F ) ~~> ( ~~> ` seq 1 ( + , F ) ) )
31 eleq1w 
 |-  ( n = j -> ( n e. Prime <-> j e. Prime ) )
32 oveq2 
 |-  ( n = j -> ( 1 / n ) = ( 1 / j ) )
33 31 32 ifbieq1d 
 |-  ( n = j -> if ( n e. Prime , ( 1 / n ) , 0 ) = if ( j e. Prime , ( 1 / j ) , 0 ) )
34 prmnn 
 |-  ( j e. Prime -> j e. NN )
35 34 adantl 
 |-  ( ( T. /\ j e. Prime ) -> j e. NN )
36 35 nnrecred 
 |-  ( ( T. /\ j e. Prime ) -> ( 1 / j ) e. RR )
37 6 a1i 
 |-  ( ( T. /\ -. j e. Prime ) -> 0 e. RR )
38 36 37 ifclda 
 |-  ( T. -> if ( j e. Prime , ( 1 / j ) , 0 ) e. RR )
39 38 mptru 
 |-  if ( j e. Prime , ( 1 / j ) , 0 ) e. RR
40 39 elexi 
 |-  if ( j e. Prime , ( 1 / j ) , 0 ) e. _V
41 33 1 40 fvmpt 
 |-  ( j e. NN -> ( F ` j ) = if ( j e. Prime , ( 1 / j ) , 0 ) )
42 41 adantl 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ j e. NN ) -> ( F ` j ) = if ( j e. Prime , ( 1 / j ) , 0 ) )
43 39 a1i 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ j e. NN ) -> if ( j e. Prime , ( 1 / j ) , 0 ) e. RR )
44 42 43 eqeltrd 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ j e. NN ) -> ( F ` j ) e. RR )
45 44 adantlr 
 |-  ( ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) /\ j e. NN ) -> ( F ` j ) e. RR )
46 nnrp 
 |-  ( j e. NN -> j e. RR+ )
47 46 adantl 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ j e. NN ) -> j e. RR+ )
48 47 rpreccld 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ j e. NN ) -> ( 1 / j ) e. RR+ )
49 48 rpge0d 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ j e. NN ) -> 0 <_ ( 1 / j ) )
50 0le0 
 |-  0 <_ 0
51 breq2 
 |-  ( ( 1 / j ) = if ( j e. Prime , ( 1 / j ) , 0 ) -> ( 0 <_ ( 1 / j ) <-> 0 <_ if ( j e. Prime , ( 1 / j ) , 0 ) ) )
52 breq2 
 |-  ( 0 = if ( j e. Prime , ( 1 / j ) , 0 ) -> ( 0 <_ 0 <-> 0 <_ if ( j e. Prime , ( 1 / j ) , 0 ) ) )
53 51 52 ifboth 
 |-  ( ( 0 <_ ( 1 / j ) /\ 0 <_ 0 ) -> 0 <_ if ( j e. Prime , ( 1 / j ) , 0 ) )
54 49 50 53 sylancl 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ j e. NN ) -> 0 <_ if ( j e. Prime , ( 1 / j ) , 0 ) )
55 54 42 breqtrrd 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ j e. NN ) -> 0 <_ ( F ` j ) )
56 55 adantlr 
 |-  ( ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) /\ j e. NN ) -> 0 <_ ( F ` j ) )
57 2 29 30 45 56 climserle 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( seq 1 ( + , F ) ` k ) <_ ( ~~> ` seq 1 ( + , F ) ) )
58 57 ralrimiva 
 |-  ( seq 1 ( + , F ) e. dom ~~> -> A. k e. NN ( seq 1 ( + , F ) ` k ) <_ ( ~~> ` seq 1 ( + , F ) ) )
59 brralrspcev 
 |-  ( ( ( ~~> ` seq 1 ( + , F ) ) e. RR /\ A. k e. NN ( seq 1 ( + , F ) ` k ) <_ ( ~~> ` seq 1 ( + , F ) ) ) -> E. x e. RR A. k e. NN ( seq 1 ( + , F ) ` k ) <_ x )
60 28 58 59 syl2anc 
 |-  ( seq 1 ( + , F ) e. dom ~~> -> E. x e. RR A. k e. NN ( seq 1 ( + , F ) ` k ) <_ x )
61 ffn 
 |-  ( seq 1 ( + , F ) : NN --> RR -> seq 1 ( + , F ) Fn NN )
62 breq1 
 |-  ( z = ( seq 1 ( + , F ) ` k ) -> ( z <_ x <-> ( seq 1 ( + , F ) ` k ) <_ x ) )
63 62 ralrn 
 |-  ( seq 1 ( + , F ) Fn NN -> ( A. z e. ran seq 1 ( + , F ) z <_ x <-> A. k e. NN ( seq 1 ( + , F ) ` k ) <_ x ) )
64 12 61 63 mp2b 
 |-  ( A. z e. ran seq 1 ( + , F ) z <_ x <-> A. k e. NN ( seq 1 ( + , F ) ` k ) <_ x )
65 64 rexbii 
 |-  ( E. x e. RR A. z e. ran seq 1 ( + , F ) z <_ x <-> E. x e. RR A. k e. NN ( seq 1 ( + , F ) ` k ) <_ x )
66 60 65 sylibr 
 |-  ( seq 1 ( + , F ) e. dom ~~> -> E. x e. RR A. z e. ran seq 1 ( + , F ) z <_ x )
67 14 22 66 suprcld 
 |-  ( seq 1 ( + , F ) e. dom ~~> -> sup ( ran seq 1 ( + , F ) , RR , < ) e. RR )
68 2rp 
 |-  2 e. RR+
69 rpreccl 
 |-  ( 2 e. RR+ -> ( 1 / 2 ) e. RR+ )
70 68 69 ax-mp 
 |-  ( 1 / 2 ) e. RR+
71 ltsubrp 
 |-  ( ( sup ( ran seq 1 ( + , F ) , RR , < ) e. RR /\ ( 1 / 2 ) e. RR+ ) -> ( sup ( ran seq 1 ( + , F ) , RR , < ) - ( 1 / 2 ) ) < sup ( ran seq 1 ( + , F ) , RR , < ) )
72 67 70 71 sylancl 
 |-  ( seq 1 ( + , F ) e. dom ~~> -> ( sup ( ran seq 1 ( + , F ) , RR , < ) - ( 1 / 2 ) ) < sup ( ran seq 1 ( + , F ) , RR , < ) )
73 halfre 
 |-  ( 1 / 2 ) e. RR
74 resubcl 
 |-  ( ( sup ( ran seq 1 ( + , F ) , RR , < ) e. RR /\ ( 1 / 2 ) e. RR ) -> ( sup ( ran seq 1 ( + , F ) , RR , < ) - ( 1 / 2 ) ) e. RR )
75 67 73 74 sylancl 
 |-  ( seq 1 ( + , F ) e. dom ~~> -> ( sup ( ran seq 1 ( + , F ) , RR , < ) - ( 1 / 2 ) ) e. RR )
76 suprlub 
 |-  ( ( ( ran seq 1 ( + , F ) C_ RR /\ ran seq 1 ( + , F ) =/= (/) /\ E. x e. RR A. z e. ran seq 1 ( + , F ) z <_ x ) /\ ( sup ( ran seq 1 ( + , F ) , RR , < ) - ( 1 / 2 ) ) e. RR ) -> ( ( sup ( ran seq 1 ( + , F ) , RR , < ) - ( 1 / 2 ) ) < sup ( ran seq 1 ( + , F ) , RR , < ) <-> E. y e. ran seq 1 ( + , F ) ( sup ( ran seq 1 ( + , F ) , RR , < ) - ( 1 / 2 ) ) < y ) )
77 14 22 66 75 76 syl31anc 
 |-  ( seq 1 ( + , F ) e. dom ~~> -> ( ( sup ( ran seq 1 ( + , F ) , RR , < ) - ( 1 / 2 ) ) < sup ( ran seq 1 ( + , F ) , RR , < ) <-> E. y e. ran seq 1 ( + , F ) ( sup ( ran seq 1 ( + , F ) , RR , < ) - ( 1 / 2 ) ) < y ) )
78 72 77 mpbid 
 |-  ( seq 1 ( + , F ) e. dom ~~> -> E. y e. ran seq 1 ( + , F ) ( sup ( ran seq 1 ( + , F ) , RR , < ) - ( 1 / 2 ) ) < y )
79 breq2 
 |-  ( y = ( seq 1 ( + , F ) ` k ) -> ( ( sup ( ran seq 1 ( + , F ) , RR , < ) - ( 1 / 2 ) ) < y <-> ( sup ( ran seq 1 ( + , F ) , RR , < ) - ( 1 / 2 ) ) < ( seq 1 ( + , F ) ` k ) ) )
80 79 rexrn 
 |-  ( seq 1 ( + , F ) Fn NN -> ( E. y e. ran seq 1 ( + , F ) ( sup ( ran seq 1 ( + , F ) , RR , < ) - ( 1 / 2 ) ) < y <-> E. k e. NN ( sup ( ran seq 1 ( + , F ) , RR , < ) - ( 1 / 2 ) ) < ( seq 1 ( + , F ) ` k ) ) )
81 12 61 80 mp2b 
 |-  ( E. y e. ran seq 1 ( + , F ) ( sup ( ran seq 1 ( + , F ) , RR , < ) - ( 1 / 2 ) ) < y <-> E. k e. NN ( sup ( ran seq 1 ( + , F ) , RR , < ) - ( 1 / 2 ) ) < ( seq 1 ( + , F ) ` k ) )
82 78 81 sylib 
 |-  ( seq 1 ( + , F ) e. dom ~~> -> E. k e. NN ( sup ( ran seq 1 ( + , F ) , RR , < ) - ( 1 / 2 ) ) < ( seq 1 ( + , F ) ` k ) )
83 2re 
 |-  2 e. RR
84 2nn 
 |-  2 e. NN
85 nnmulcl 
 |-  ( ( 2 e. NN /\ k e. NN ) -> ( 2 x. k ) e. NN )
86 84 29 85 sylancr 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( 2 x. k ) e. NN )
87 86 peano2nnd 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( ( 2 x. k ) + 1 ) e. NN )
88 87 nnnn0d 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( ( 2 x. k ) + 1 ) e. NN0 )
89 reexpcl 
 |-  ( ( 2 e. RR /\ ( ( 2 x. k ) + 1 ) e. NN0 ) -> ( 2 ^ ( ( 2 x. k ) + 1 ) ) e. RR )
90 83 88 89 sylancr 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( 2 ^ ( ( 2 x. k ) + 1 ) ) e. RR )
91 90 ltnrd 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> -. ( 2 ^ ( ( 2 x. k ) + 1 ) ) < ( 2 ^ ( ( 2 x. k ) + 1 ) ) )
92 29 adantr 
 |-  ( ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) /\ sum_ j e. ( ZZ>= ` ( k + 1 ) ) if ( j e. Prime , ( 1 / j ) , 0 ) < ( 1 / 2 ) ) -> k e. NN )
93 peano2nn 
 |-  ( k e. NN -> ( k + 1 ) e. NN )
94 93 adantl 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( k + 1 ) e. NN )
95 94 nnnn0d 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( k + 1 ) e. NN0 )
96 nnexpcl 
 |-  ( ( 2 e. NN /\ ( k + 1 ) e. NN0 ) -> ( 2 ^ ( k + 1 ) ) e. NN )
97 84 95 96 sylancr 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( 2 ^ ( k + 1 ) ) e. NN )
98 97 nnsqcld 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( ( 2 ^ ( k + 1 ) ) ^ 2 ) e. NN )
99 98 adantr 
 |-  ( ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) /\ sum_ j e. ( ZZ>= ` ( k + 1 ) ) if ( j e. Prime , ( 1 / j ) , 0 ) < ( 1 / 2 ) ) -> ( ( 2 ^ ( k + 1 ) ) ^ 2 ) e. NN )
100 breq1 
 |-  ( p = w -> ( p || r <-> w || r ) )
101 100 notbid 
 |-  ( p = w -> ( -. p || r <-> -. w || r ) )
102 101 cbvralvw 
 |-  ( A. p e. ( Prime \ ( 1 ... k ) ) -. p || r <-> A. w e. ( Prime \ ( 1 ... k ) ) -. w || r )
103 breq2 
 |-  ( r = n -> ( w || r <-> w || n ) )
104 103 notbid 
 |-  ( r = n -> ( -. w || r <-> -. w || n ) )
105 104 ralbidv 
 |-  ( r = n -> ( A. w e. ( Prime \ ( 1 ... k ) ) -. w || r <-> A. w e. ( Prime \ ( 1 ... k ) ) -. w || n ) )
106 102 105 bitrid 
 |-  ( r = n -> ( A. p e. ( Prime \ ( 1 ... k ) ) -. p || r <-> A. w e. ( Prime \ ( 1 ... k ) ) -. w || n ) )
107 106 cbvrabv 
 |-  { r e. ( 1 ... ( ( 2 ^ ( k + 1 ) ) ^ 2 ) ) | A. p e. ( Prime \ ( 1 ... k ) ) -. p || r } = { n e. ( 1 ... ( ( 2 ^ ( k + 1 ) ) ^ 2 ) ) | A. w e. ( Prime \ ( 1 ... k ) ) -. w || n }
108 simpll 
 |-  ( ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) /\ sum_ j e. ( ZZ>= ` ( k + 1 ) ) if ( j e. Prime , ( 1 / j ) , 0 ) < ( 1 / 2 ) ) -> seq 1 ( + , F ) e. dom ~~> )
109 eleq1w 
 |-  ( m = j -> ( m e. Prime <-> j e. Prime ) )
110 oveq2 
 |-  ( m = j -> ( 1 / m ) = ( 1 / j ) )
111 109 110 ifbieq1d 
 |-  ( m = j -> if ( m e. Prime , ( 1 / m ) , 0 ) = if ( j e. Prime , ( 1 / j ) , 0 ) )
112 111 cbvsumv 
 |-  sum_ m e. ( ZZ>= ` ( k + 1 ) ) if ( m e. Prime , ( 1 / m ) , 0 ) = sum_ j e. ( ZZ>= ` ( k + 1 ) ) if ( j e. Prime , ( 1 / j ) , 0 )
113 simpr 
 |-  ( ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) /\ sum_ j e. ( ZZ>= ` ( k + 1 ) ) if ( j e. Prime , ( 1 / j ) , 0 ) < ( 1 / 2 ) ) -> sum_ j e. ( ZZ>= ` ( k + 1 ) ) if ( j e. Prime , ( 1 / j ) , 0 ) < ( 1 / 2 ) )
114 112 113 eqbrtrid 
 |-  ( ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) /\ sum_ j e. ( ZZ>= ` ( k + 1 ) ) if ( j e. Prime , ( 1 / j ) , 0 ) < ( 1 / 2 ) ) -> sum_ m e. ( ZZ>= ` ( k + 1 ) ) if ( m e. Prime , ( 1 / m ) , 0 ) < ( 1 / 2 ) )
115 eqid 
 |-  ( w e. NN |-> { n e. ( 1 ... ( ( 2 ^ ( k + 1 ) ) ^ 2 ) ) | ( w e. Prime /\ w || n ) } ) = ( w e. NN |-> { n e. ( 1 ... ( ( 2 ^ ( k + 1 ) ) ^ 2 ) ) | ( w e. Prime /\ w || n ) } )
116 1 92 99 107 108 114 115 prmreclem5 
 |-  ( ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) /\ sum_ j e. ( ZZ>= ` ( k + 1 ) ) if ( j e. Prime , ( 1 / j ) , 0 ) < ( 1 / 2 ) ) -> ( ( ( 2 ^ ( k + 1 ) ) ^ 2 ) / 2 ) < ( ( 2 ^ k ) x. ( sqrt ` ( ( 2 ^ ( k + 1 ) ) ^ 2 ) ) ) )
117 116 ex 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( sum_ j e. ( ZZ>= ` ( k + 1 ) ) if ( j e. Prime , ( 1 / j ) , 0 ) < ( 1 / 2 ) -> ( ( ( 2 ^ ( k + 1 ) ) ^ 2 ) / 2 ) < ( ( 2 ^ k ) x. ( sqrt ` ( ( 2 ^ ( k + 1 ) ) ^ 2 ) ) ) ) )
118 eqid 
 |-  ( ZZ>= ` ( k + 1 ) ) = ( ZZ>= ` ( k + 1 ) )
119 94 nnzd 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( k + 1 ) e. ZZ )
120 eluznn 
 |-  ( ( ( k + 1 ) e. NN /\ j e. ( ZZ>= ` ( k + 1 ) ) ) -> j e. NN )
121 94 120 sylan 
 |-  ( ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) /\ j e. ( ZZ>= ` ( k + 1 ) ) ) -> j e. NN )
122 121 41 syl 
 |-  ( ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) /\ j e. ( ZZ>= ` ( k + 1 ) ) ) -> ( F ` j ) = if ( j e. Prime , ( 1 / j ) , 0 ) )
123 39 a1i 
 |-  ( ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) /\ j e. ( ZZ>= ` ( k + 1 ) ) ) -> if ( j e. Prime , ( 1 / j ) , 0 ) e. RR )
124 simpl 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> seq 1 ( + , F ) e. dom ~~> )
125 41 adantl 
 |-  ( ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) /\ j e. NN ) -> ( F ` j ) = if ( j e. Prime , ( 1 / j ) , 0 ) )
126 39 recni 
 |-  if ( j e. Prime , ( 1 / j ) , 0 ) e. CC
127 126 a1i 
 |-  ( ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) /\ j e. NN ) -> if ( j e. Prime , ( 1 / j ) , 0 ) e. CC )
128 125 127 eqeltrd 
 |-  ( ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) /\ j e. NN ) -> ( F ` j ) e. CC )
129 2 94 128 iserex 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( seq 1 ( + , F ) e. dom ~~> <-> seq ( k + 1 ) ( + , F ) e. dom ~~> ) )
130 124 129 mpbid 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> seq ( k + 1 ) ( + , F ) e. dom ~~> )
131 118 119 122 123 130 isumrecl 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> sum_ j e. ( ZZ>= ` ( k + 1 ) ) if ( j e. Prime , ( 1 / j ) , 0 ) e. RR )
132 73 a1i 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( 1 / 2 ) e. RR )
133 elfznn 
 |-  ( j e. ( 1 ... k ) -> j e. NN )
134 133 adantl 
 |-  ( ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> j e. NN )
135 134 41 syl 
 |-  ( ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> ( F ` j ) = if ( j e. Prime , ( 1 / j ) , 0 ) )
136 29 2 eleqtrdi 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> k e. ( ZZ>= ` 1 ) )
137 126 a1i 
 |-  ( ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> if ( j e. Prime , ( 1 / j ) , 0 ) e. CC )
138 135 136 137 fsumser 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> sum_ j e. ( 1 ... k ) if ( j e. Prime , ( 1 / j ) , 0 ) = ( seq 1 ( + , F ) ` k ) )
139 138 27 eqeltrd 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> sum_ j e. ( 1 ... k ) if ( j e. Prime , ( 1 / j ) , 0 ) e. RR )
140 131 132 139 ltadd2d 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( sum_ j e. ( ZZ>= ` ( k + 1 ) ) if ( j e. Prime , ( 1 / j ) , 0 ) < ( 1 / 2 ) <-> ( sum_ j e. ( 1 ... k ) if ( j e. Prime , ( 1 / j ) , 0 ) + sum_ j e. ( ZZ>= ` ( k + 1 ) ) if ( j e. Prime , ( 1 / j ) , 0 ) ) < ( sum_ j e. ( 1 ... k ) if ( j e. Prime , ( 1 / j ) , 0 ) + ( 1 / 2 ) ) ) )
141 2 118 94 125 127 124 isumsplit 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> sum_ j e. NN if ( j e. Prime , ( 1 / j ) , 0 ) = ( sum_ j e. ( 1 ... ( ( k + 1 ) - 1 ) ) if ( j e. Prime , ( 1 / j ) , 0 ) + sum_ j e. ( ZZ>= ` ( k + 1 ) ) if ( j e. Prime , ( 1 / j ) , 0 ) ) )
142 nncn 
 |-  ( k e. NN -> k e. CC )
143 142 adantl 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> k e. CC )
144 ax-1cn 
 |-  1 e. CC
145 pncan 
 |-  ( ( k e. CC /\ 1 e. CC ) -> ( ( k + 1 ) - 1 ) = k )
146 143 144 145 sylancl 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( ( k + 1 ) - 1 ) = k )
147 146 oveq2d 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( 1 ... ( ( k + 1 ) - 1 ) ) = ( 1 ... k ) )
148 147 sumeq1d 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> sum_ j e. ( 1 ... ( ( k + 1 ) - 1 ) ) if ( j e. Prime , ( 1 / j ) , 0 ) = sum_ j e. ( 1 ... k ) if ( j e. Prime , ( 1 / j ) , 0 ) )
149 148 oveq1d 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( sum_ j e. ( 1 ... ( ( k + 1 ) - 1 ) ) if ( j e. Prime , ( 1 / j ) , 0 ) + sum_ j e. ( ZZ>= ` ( k + 1 ) ) if ( j e. Prime , ( 1 / j ) , 0 ) ) = ( sum_ j e. ( 1 ... k ) if ( j e. Prime , ( 1 / j ) , 0 ) + sum_ j e. ( ZZ>= ` ( k + 1 ) ) if ( j e. Prime , ( 1 / j ) , 0 ) ) )
150 141 149 eqtrd 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> sum_ j e. NN if ( j e. Prime , ( 1 / j ) , 0 ) = ( sum_ j e. ( 1 ... k ) if ( j e. Prime , ( 1 / j ) , 0 ) + sum_ j e. ( ZZ>= ` ( k + 1 ) ) if ( j e. Prime , ( 1 / j ) , 0 ) ) )
151 150 breq1d 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( sum_ j e. NN if ( j e. Prime , ( 1 / j ) , 0 ) < ( sum_ j e. ( 1 ... k ) if ( j e. Prime , ( 1 / j ) , 0 ) + ( 1 / 2 ) ) <-> ( sum_ j e. ( 1 ... k ) if ( j e. Prime , ( 1 / j ) , 0 ) + sum_ j e. ( ZZ>= ` ( k + 1 ) ) if ( j e. Prime , ( 1 / j ) , 0 ) ) < ( sum_ j e. ( 1 ... k ) if ( j e. Prime , ( 1 / j ) , 0 ) + ( 1 / 2 ) ) ) )
152 140 151 bitr4d 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( sum_ j e. ( ZZ>= ` ( k + 1 ) ) if ( j e. Prime , ( 1 / j ) , 0 ) < ( 1 / 2 ) <-> sum_ j e. NN if ( j e. Prime , ( 1 / j ) , 0 ) < ( sum_ j e. ( 1 ... k ) if ( j e. Prime , ( 1 / j ) , 0 ) + ( 1 / 2 ) ) ) )
153 eqid 
 |-  seq 1 ( + , F ) = seq 1 ( + , F )
154 2 153 23 42 43 54 60 isumsup 
 |-  ( seq 1 ( + , F ) e. dom ~~> -> sum_ j e. NN if ( j e. Prime , ( 1 / j ) , 0 ) = sup ( ran seq 1 ( + , F ) , RR , < ) )
155 154 67 eqeltrd 
 |-  ( seq 1 ( + , F ) e. dom ~~> -> sum_ j e. NN if ( j e. Prime , ( 1 / j ) , 0 ) e. RR )
156 155 adantr 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> sum_ j e. NN if ( j e. Prime , ( 1 / j ) , 0 ) e. RR )
157 156 132 139 ltsubaddd 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( ( sum_ j e. NN if ( j e. Prime , ( 1 / j ) , 0 ) - ( 1 / 2 ) ) < sum_ j e. ( 1 ... k ) if ( j e. Prime , ( 1 / j ) , 0 ) <-> sum_ j e. NN if ( j e. Prime , ( 1 / j ) , 0 ) < ( sum_ j e. ( 1 ... k ) if ( j e. Prime , ( 1 / j ) , 0 ) + ( 1 / 2 ) ) ) )
158 154 adantr 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> sum_ j e. NN if ( j e. Prime , ( 1 / j ) , 0 ) = sup ( ran seq 1 ( + , F ) , RR , < ) )
159 158 oveq1d 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( sum_ j e. NN if ( j e. Prime , ( 1 / j ) , 0 ) - ( 1 / 2 ) ) = ( sup ( ran seq 1 ( + , F ) , RR , < ) - ( 1 / 2 ) ) )
160 159 138 breq12d 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( ( sum_ j e. NN if ( j e. Prime , ( 1 / j ) , 0 ) - ( 1 / 2 ) ) < sum_ j e. ( 1 ... k ) if ( j e. Prime , ( 1 / j ) , 0 ) <-> ( sup ( ran seq 1 ( + , F ) , RR , < ) - ( 1 / 2 ) ) < ( seq 1 ( + , F ) ` k ) ) )
161 152 157 160 3bitr2d 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( sum_ j e. ( ZZ>= ` ( k + 1 ) ) if ( j e. Prime , ( 1 / j ) , 0 ) < ( 1 / 2 ) <-> ( sup ( ran seq 1 ( + , F ) , RR , < ) - ( 1 / 2 ) ) < ( seq 1 ( + , F ) ` k ) ) )
162 2cn 
 |-  2 e. CC
163 162 a1i 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> 2 e. CC )
164 144 a1i 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> 1 e. CC )
165 163 143 164 adddid 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( 2 x. ( k + 1 ) ) = ( ( 2 x. k ) + ( 2 x. 1 ) ) )
166 94 nncnd 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( k + 1 ) e. CC )
167 mulcom 
 |-  ( ( ( k + 1 ) e. CC /\ 2 e. CC ) -> ( ( k + 1 ) x. 2 ) = ( 2 x. ( k + 1 ) ) )
168 166 162 167 sylancl 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( ( k + 1 ) x. 2 ) = ( 2 x. ( k + 1 ) ) )
169 86 nncnd 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( 2 x. k ) e. CC )
170 169 164 164 addassd 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( ( ( 2 x. k ) + 1 ) + 1 ) = ( ( 2 x. k ) + ( 1 + 1 ) ) )
171 144 2timesi 
 |-  ( 2 x. 1 ) = ( 1 + 1 )
172 171 oveq2i 
 |-  ( ( 2 x. k ) + ( 2 x. 1 ) ) = ( ( 2 x. k ) + ( 1 + 1 ) )
173 170 172 eqtr4di 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( ( ( 2 x. k ) + 1 ) + 1 ) = ( ( 2 x. k ) + ( 2 x. 1 ) ) )
174 165 168 173 3eqtr4d 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( ( k + 1 ) x. 2 ) = ( ( ( 2 x. k ) + 1 ) + 1 ) )
175 174 oveq2d 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( 2 ^ ( ( k + 1 ) x. 2 ) ) = ( 2 ^ ( ( ( 2 x. k ) + 1 ) + 1 ) ) )
176 2nn0 
 |-  2 e. NN0
177 176 a1i 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> 2 e. NN0 )
178 163 177 95 expmuld 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( 2 ^ ( ( k + 1 ) x. 2 ) ) = ( ( 2 ^ ( k + 1 ) ) ^ 2 ) )
179 expp1 
 |-  ( ( 2 e. CC /\ ( ( 2 x. k ) + 1 ) e. NN0 ) -> ( 2 ^ ( ( ( 2 x. k ) + 1 ) + 1 ) ) = ( ( 2 ^ ( ( 2 x. k ) + 1 ) ) x. 2 ) )
180 162 88 179 sylancr 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( 2 ^ ( ( ( 2 x. k ) + 1 ) + 1 ) ) = ( ( 2 ^ ( ( 2 x. k ) + 1 ) ) x. 2 ) )
181 175 178 180 3eqtr3d 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( ( 2 ^ ( k + 1 ) ) ^ 2 ) = ( ( 2 ^ ( ( 2 x. k ) + 1 ) ) x. 2 ) )
182 181 oveq1d 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( ( ( 2 ^ ( k + 1 ) ) ^ 2 ) / 2 ) = ( ( ( 2 ^ ( ( 2 x. k ) + 1 ) ) x. 2 ) / 2 ) )
183 expcl 
 |-  ( ( 2 e. CC /\ ( ( 2 x. k ) + 1 ) e. NN0 ) -> ( 2 ^ ( ( 2 x. k ) + 1 ) ) e. CC )
184 162 88 183 sylancr 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( 2 ^ ( ( 2 x. k ) + 1 ) ) e. CC )
185 2ne0 
 |-  2 =/= 0
186 divcan4 
 |-  ( ( ( 2 ^ ( ( 2 x. k ) + 1 ) ) e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( ( ( 2 ^ ( ( 2 x. k ) + 1 ) ) x. 2 ) / 2 ) = ( 2 ^ ( ( 2 x. k ) + 1 ) ) )
187 162 185 186 mp3an23 
 |-  ( ( 2 ^ ( ( 2 x. k ) + 1 ) ) e. CC -> ( ( ( 2 ^ ( ( 2 x. k ) + 1 ) ) x. 2 ) / 2 ) = ( 2 ^ ( ( 2 x. k ) + 1 ) ) )
188 184 187 syl 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( ( ( 2 ^ ( ( 2 x. k ) + 1 ) ) x. 2 ) / 2 ) = ( 2 ^ ( ( 2 x. k ) + 1 ) ) )
189 182 188 eqtrd 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( ( ( 2 ^ ( k + 1 ) ) ^ 2 ) / 2 ) = ( 2 ^ ( ( 2 x. k ) + 1 ) ) )
190 nnnn0 
 |-  ( k e. NN -> k e. NN0 )
191 190 adantl 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> k e. NN0 )
192 163 95 191 expaddd 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( 2 ^ ( k + ( k + 1 ) ) ) = ( ( 2 ^ k ) x. ( 2 ^ ( k + 1 ) ) ) )
193 143 2timesd 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( 2 x. k ) = ( k + k ) )
194 193 oveq1d 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( ( 2 x. k ) + 1 ) = ( ( k + k ) + 1 ) )
195 143 143 164 addassd 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( ( k + k ) + 1 ) = ( k + ( k + 1 ) ) )
196 194 195 eqtrd 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( ( 2 x. k ) + 1 ) = ( k + ( k + 1 ) ) )
197 196 oveq2d 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( 2 ^ ( ( 2 x. k ) + 1 ) ) = ( 2 ^ ( k + ( k + 1 ) ) ) )
198 97 nnrpd 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( 2 ^ ( k + 1 ) ) e. RR+ )
199 198 rprege0d 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( ( 2 ^ ( k + 1 ) ) e. RR /\ 0 <_ ( 2 ^ ( k + 1 ) ) ) )
200 sqrtsq 
 |-  ( ( ( 2 ^ ( k + 1 ) ) e. RR /\ 0 <_ ( 2 ^ ( k + 1 ) ) ) -> ( sqrt ` ( ( 2 ^ ( k + 1 ) ) ^ 2 ) ) = ( 2 ^ ( k + 1 ) ) )
201 199 200 syl 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( sqrt ` ( ( 2 ^ ( k + 1 ) ) ^ 2 ) ) = ( 2 ^ ( k + 1 ) ) )
202 201 oveq2d 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( ( 2 ^ k ) x. ( sqrt ` ( ( 2 ^ ( k + 1 ) ) ^ 2 ) ) ) = ( ( 2 ^ k ) x. ( 2 ^ ( k + 1 ) ) ) )
203 192 197 202 3eqtr4rd 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( ( 2 ^ k ) x. ( sqrt ` ( ( 2 ^ ( k + 1 ) ) ^ 2 ) ) ) = ( 2 ^ ( ( 2 x. k ) + 1 ) ) )
204 189 203 breq12d 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( ( ( ( 2 ^ ( k + 1 ) ) ^ 2 ) / 2 ) < ( ( 2 ^ k ) x. ( sqrt ` ( ( 2 ^ ( k + 1 ) ) ^ 2 ) ) ) <-> ( 2 ^ ( ( 2 x. k ) + 1 ) ) < ( 2 ^ ( ( 2 x. k ) + 1 ) ) ) )
205 117 161 204 3imtr3d 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> ( ( sup ( ran seq 1 ( + , F ) , RR , < ) - ( 1 / 2 ) ) < ( seq 1 ( + , F ) ` k ) -> ( 2 ^ ( ( 2 x. k ) + 1 ) ) < ( 2 ^ ( ( 2 x. k ) + 1 ) ) ) )
206 91 205 mtod 
 |-  ( ( seq 1 ( + , F ) e. dom ~~> /\ k e. NN ) -> -. ( sup ( ran seq 1 ( + , F ) , RR , < ) - ( 1 / 2 ) ) < ( seq 1 ( + , F ) ` k ) )
207 206 nrexdv 
 |-  ( seq 1 ( + , F ) e. dom ~~> -> -. E. k e. NN ( sup ( ran seq 1 ( + , F ) , RR , < ) - ( 1 / 2 ) ) < ( seq 1 ( + , F ) ` k ) )
208 82 207 pm2.65i 
 |-  -. seq 1 ( + , F ) e. dom ~~>