Metamath Proof Explorer


Theorem dchrisum0fno1

Description: The sum sum_ k <_ x , F ( x ) / sqrt k is divergent (i.e. not eventually bounded). Equation 9.4.30 of Shapiro, p. 383. (Contributed by Mario Carneiro, 5-May-2016)

Ref Expression
Hypotheses rpvmasum.z 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
rpvmasum.l 𝐿 = ( ℤRHom ‘ 𝑍 )
rpvmasum.a ( 𝜑𝑁 ∈ ℕ )
rpvmasum2.g 𝐺 = ( DChr ‘ 𝑁 )
rpvmasum2.d 𝐷 = ( Base ‘ 𝐺 )
rpvmasum2.1 1 = ( 0g𝐺 )
dchrisum0f.f 𝐹 = ( 𝑏 ∈ ℕ ↦ Σ 𝑣 ∈ { 𝑞 ∈ ℕ ∣ 𝑞𝑏 } ( 𝑋 ‘ ( 𝐿𝑣 ) ) )
dchrisum0f.x ( 𝜑𝑋𝐷 )
dchrisum0flb.r ( 𝜑𝑋 : ( Base ‘ 𝑍 ) ⟶ ℝ )
dchrisum0fno1.a ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝐹𝑘 ) / ( √ ‘ 𝑘 ) ) ) ∈ 𝑂(1) )
Assertion dchrisum0fno1 ¬ 𝜑

Proof

Step Hyp Ref Expression
1 rpvmasum.z 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
2 rpvmasum.l 𝐿 = ( ℤRHom ‘ 𝑍 )
3 rpvmasum.a ( 𝜑𝑁 ∈ ℕ )
4 rpvmasum2.g 𝐺 = ( DChr ‘ 𝑁 )
5 rpvmasum2.d 𝐷 = ( Base ‘ 𝐺 )
6 rpvmasum2.1 1 = ( 0g𝐺 )
7 dchrisum0f.f 𝐹 = ( 𝑏 ∈ ℕ ↦ Σ 𝑣 ∈ { 𝑞 ∈ ℕ ∣ 𝑞𝑏 } ( 𝑋 ‘ ( 𝐿𝑣 ) ) )
8 dchrisum0f.x ( 𝜑𝑋𝐷 )
9 dchrisum0flb.r ( 𝜑𝑋 : ( Base ‘ 𝑍 ) ⟶ ℝ )
10 dchrisum0fno1.a ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝐹𝑘 ) / ( √ ‘ 𝑘 ) ) ) ∈ 𝑂(1) )
11 logno1 ¬ ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ 𝑂(1)
12 relogcl ( 𝑥 ∈ ℝ+ → ( log ‘ 𝑥 ) ∈ ℝ )
13 12 adantl ( ( 𝜑𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℝ )
14 13 recnd ( ( 𝜑𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℂ )
15 2cnd ( ( 𝜑𝑥 ∈ ℝ+ ) → 2 ∈ ℂ )
16 2ne0 2 ≠ 0
17 16 a1i ( ( 𝜑𝑥 ∈ ℝ+ ) → 2 ≠ 0 )
18 14 15 17 divcan2d ( ( 𝜑𝑥 ∈ ℝ+ ) → ( 2 · ( ( log ‘ 𝑥 ) / 2 ) ) = ( log ‘ 𝑥 ) )
19 18 mpteq2dva ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( 2 · ( ( log ‘ 𝑥 ) / 2 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) )
20 13 rehalfcld ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) / 2 ) ∈ ℝ )
21 20 recnd ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) / 2 ) ∈ ℂ )
22 rpssre + ⊆ ℝ
23 2cn 2 ∈ ℂ
24 o1const ( ( ℝ+ ⊆ ℝ ∧ 2 ∈ ℂ ) → ( 𝑥 ∈ ℝ+ ↦ 2 ) ∈ 𝑂(1) )
25 22 23 24 mp2an ( 𝑥 ∈ ℝ+ ↦ 2 ) ∈ 𝑂(1)
26 25 a1i ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ 2 ) ∈ 𝑂(1) )
27 1red ( 𝜑 → 1 ∈ ℝ )
28 sumex Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝐹𝑘 ) / ( √ ‘ 𝑘 ) ) ∈ V
29 28 a1i ( ( 𝜑𝑥 ∈ ℝ+ ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝐹𝑘 ) / ( √ ‘ 𝑘 ) ) ∈ V )
30 20 adantrr ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( log ‘ 𝑥 ) / 2 ) ∈ ℝ )
31 12 ad2antrl ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( log ‘ 𝑥 ) ∈ ℝ )
32 log1 ( log ‘ 1 ) = 0
33 simprr ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 1 ≤ 𝑥 )
34 1rp 1 ∈ ℝ+
35 simprl ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ+ )
36 logleb ( ( 1 ∈ ℝ+𝑥 ∈ ℝ+ ) → ( 1 ≤ 𝑥 ↔ ( log ‘ 1 ) ≤ ( log ‘ 𝑥 ) ) )
37 34 35 36 sylancr ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 1 ≤ 𝑥 ↔ ( log ‘ 1 ) ≤ ( log ‘ 𝑥 ) ) )
38 33 37 mpbid ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( log ‘ 1 ) ≤ ( log ‘ 𝑥 ) )
39 32 38 eqbrtrrid ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 0 ≤ ( log ‘ 𝑥 ) )
40 2re 2 ∈ ℝ
41 40 a1i ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 2 ∈ ℝ )
42 2pos 0 < 2
43 42 a1i ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 0 < 2 )
44 divge0 ( ( ( ( log ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( log ‘ 𝑥 ) ) ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → 0 ≤ ( ( log ‘ 𝑥 ) / 2 ) )
45 31 39 41 43 44 syl22anc ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 0 ≤ ( ( log ‘ 𝑥 ) / 2 ) )
46 30 45 absidd ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( ( log ‘ 𝑥 ) / 2 ) ) = ( ( log ‘ 𝑥 ) / 2 ) )
47 fzfid ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
48 1 2 3 4 5 6 7 8 9 dchrisum0ff ( 𝜑𝐹 : ℕ ⟶ ℝ )
49 48 adantr ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝐹 : ℕ ⟶ ℝ )
50 elfznn ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑘 ∈ ℕ )
51 ffvelrn ( ( 𝐹 : ℕ ⟶ ℝ ∧ 𝑘 ∈ ℕ ) → ( 𝐹𝑘 ) ∈ ℝ )
52 49 50 51 syl2an ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐹𝑘 ) ∈ ℝ )
53 50 adantl ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑘 ∈ ℕ )
54 53 nnrpd ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑘 ∈ ℝ+ )
55 54 rpsqrtcld ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( √ ‘ 𝑘 ) ∈ ℝ+ )
56 52 55 rerpdivcld ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝐹𝑘 ) / ( √ ‘ 𝑘 ) ) ∈ ℝ )
57 47 56 fsumrecl ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝐹𝑘 ) / ( √ ‘ 𝑘 ) ) ∈ ℝ )
58 57 recnd ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝐹𝑘 ) / ( √ ‘ 𝑘 ) ) ∈ ℂ )
59 58 abscld ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝐹𝑘 ) / ( √ ‘ 𝑘 ) ) ) ∈ ℝ )
60 fzfid ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ∈ Fin )
61 elfznn ( 𝑖 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) → 𝑖 ∈ ℕ )
62 61 adantl ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑖 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ) → 𝑖 ∈ ℕ )
63 62 nnrecred ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑖 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ) → ( 1 / 𝑖 ) ∈ ℝ )
64 60 63 fsumrecl ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ( 1 / 𝑖 ) ∈ ℝ )
65 logsqrt ( 𝑥 ∈ ℝ+ → ( log ‘ ( √ ‘ 𝑥 ) ) = ( ( log ‘ 𝑥 ) / 2 ) )
66 65 ad2antrl ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( log ‘ ( √ ‘ 𝑥 ) ) = ( ( log ‘ 𝑥 ) / 2 ) )
67 rpsqrtcl ( 𝑥 ∈ ℝ+ → ( √ ‘ 𝑥 ) ∈ ℝ+ )
68 67 ad2antrl ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( √ ‘ 𝑥 ) ∈ ℝ+ )
69 harmoniclbnd ( ( √ ‘ 𝑥 ) ∈ ℝ+ → ( log ‘ ( √ ‘ 𝑥 ) ) ≤ Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ( 1 / 𝑖 ) )
70 68 69 syl ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( log ‘ ( √ ‘ 𝑥 ) ) ≤ Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ( 1 / 𝑖 ) )
71 66 70 eqbrtrrd ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( log ‘ 𝑥 ) / 2 ) ≤ Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ( 1 / 𝑖 ) )
72 eqid ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) = ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) )
73 ovex ( 𝑚 ↑ 2 ) ∈ V
74 72 73 elrnmpti ( 𝑘 ∈ ran ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) ↔ ∃ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) 𝑘 = ( 𝑚 ↑ 2 ) )
75 elfznn ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) → 𝑚 ∈ ℕ )
76 75 adantl ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ) → 𝑚 ∈ ℕ )
77 76 nnrpd ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ) → 𝑚 ∈ ℝ+ )
78 77 rprege0d ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ) → ( 𝑚 ∈ ℝ ∧ 0 ≤ 𝑚 ) )
79 sqrtsq ( ( 𝑚 ∈ ℝ ∧ 0 ≤ 𝑚 ) → ( √ ‘ ( 𝑚 ↑ 2 ) ) = 𝑚 )
80 78 79 syl ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ) → ( √ ‘ ( 𝑚 ↑ 2 ) ) = 𝑚 )
81 80 76 eqeltrd ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ) → ( √ ‘ ( 𝑚 ↑ 2 ) ) ∈ ℕ )
82 fveq2 ( 𝑘 = ( 𝑚 ↑ 2 ) → ( √ ‘ 𝑘 ) = ( √ ‘ ( 𝑚 ↑ 2 ) ) )
83 82 eleq1d ( 𝑘 = ( 𝑚 ↑ 2 ) → ( ( √ ‘ 𝑘 ) ∈ ℕ ↔ ( √ ‘ ( 𝑚 ↑ 2 ) ) ∈ ℕ ) )
84 81 83 syl5ibrcom ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ) → ( 𝑘 = ( 𝑚 ↑ 2 ) → ( √ ‘ 𝑘 ) ∈ ℕ ) )
85 84 rexlimdva ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ∃ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) 𝑘 = ( 𝑚 ↑ 2 ) → ( √ ‘ 𝑘 ) ∈ ℕ ) )
86 74 85 syl5bi ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 𝑘 ∈ ran ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) → ( √ ‘ 𝑘 ) ∈ ℕ ) )
87 86 imp ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ran ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) ) → ( √ ‘ 𝑘 ) ∈ ℕ )
88 87 iftrued ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ran ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) ) → if ( ( √ ‘ 𝑘 ) ∈ ℕ , 1 , 0 ) = 1 )
89 88 oveq1d ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ran ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) ) → ( if ( ( √ ‘ 𝑘 ) ∈ ℕ , 1 , 0 ) / ( √ ‘ 𝑘 ) ) = ( 1 / ( √ ‘ 𝑘 ) ) )
90 89 sumeq2dv ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑘 ∈ ran ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) ( if ( ( √ ‘ 𝑘 ) ∈ ℕ , 1 , 0 ) / ( √ ‘ 𝑘 ) ) = Σ 𝑘 ∈ ran ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) ( 1 / ( √ ‘ 𝑘 ) ) )
91 fveq2 ( 𝑘 = ( 𝑖 ↑ 2 ) → ( √ ‘ 𝑘 ) = ( √ ‘ ( 𝑖 ↑ 2 ) ) )
92 91 oveq2d ( 𝑘 = ( 𝑖 ↑ 2 ) → ( 1 / ( √ ‘ 𝑘 ) ) = ( 1 / ( √ ‘ ( 𝑖 ↑ 2 ) ) ) )
93 76 nnsqcld ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ) → ( 𝑚 ↑ 2 ) ∈ ℕ )
94 68 rpred ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( √ ‘ 𝑥 ) ∈ ℝ )
95 fznnfl ( ( √ ‘ 𝑥 ) ∈ ℝ → ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↔ ( 𝑚 ∈ ℕ ∧ 𝑚 ≤ ( √ ‘ 𝑥 ) ) ) )
96 94 95 syl ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↔ ( 𝑚 ∈ ℕ ∧ 𝑚 ≤ ( √ ‘ 𝑥 ) ) ) )
97 96 simplbda ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ) → 𝑚 ≤ ( √ ‘ 𝑥 ) )
98 68 adantr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ) → ( √ ‘ 𝑥 ) ∈ ℝ+ )
99 98 rprege0d ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ) → ( ( √ ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( √ ‘ 𝑥 ) ) )
100 le2sq ( ( ( 𝑚 ∈ ℝ ∧ 0 ≤ 𝑚 ) ∧ ( ( √ ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( √ ‘ 𝑥 ) ) ) → ( 𝑚 ≤ ( √ ‘ 𝑥 ) ↔ ( 𝑚 ↑ 2 ) ≤ ( ( √ ‘ 𝑥 ) ↑ 2 ) ) )
101 78 99 100 syl2anc ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ) → ( 𝑚 ≤ ( √ ‘ 𝑥 ) ↔ ( 𝑚 ↑ 2 ) ≤ ( ( √ ‘ 𝑥 ) ↑ 2 ) ) )
102 97 101 mpbid ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ) → ( 𝑚 ↑ 2 ) ≤ ( ( √ ‘ 𝑥 ) ↑ 2 ) )
103 35 rpred ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ )
104 103 adantr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ) → 𝑥 ∈ ℝ )
105 104 recnd ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ) → 𝑥 ∈ ℂ )
106 105 sqsqrtd ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ) → ( ( √ ‘ 𝑥 ) ↑ 2 ) = 𝑥 )
107 102 106 breqtrd ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ) → ( 𝑚 ↑ 2 ) ≤ 𝑥 )
108 fznnfl ( 𝑥 ∈ ℝ → ( ( 𝑚 ↑ 2 ) ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ↔ ( ( 𝑚 ↑ 2 ) ∈ ℕ ∧ ( 𝑚 ↑ 2 ) ≤ 𝑥 ) ) )
109 104 108 syl ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ) → ( ( 𝑚 ↑ 2 ) ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ↔ ( ( 𝑚 ↑ 2 ) ∈ ℕ ∧ ( 𝑚 ↑ 2 ) ≤ 𝑥 ) ) )
110 93 107 109 mpbir2and ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ) → ( 𝑚 ↑ 2 ) ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) )
111 110 ex ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) → ( 𝑚 ↑ 2 ) ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) )
112 75 nnrpd ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) → 𝑚 ∈ ℝ+ )
113 112 rprege0d ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) → ( 𝑚 ∈ ℝ ∧ 0 ≤ 𝑚 ) )
114 61 nnrpd ( 𝑖 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) → 𝑖 ∈ ℝ+ )
115 114 rprege0d ( 𝑖 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) → ( 𝑖 ∈ ℝ ∧ 0 ≤ 𝑖 ) )
116 sq11 ( ( ( 𝑚 ∈ ℝ ∧ 0 ≤ 𝑚 ) ∧ ( 𝑖 ∈ ℝ ∧ 0 ≤ 𝑖 ) ) → ( ( 𝑚 ↑ 2 ) = ( 𝑖 ↑ 2 ) ↔ 𝑚 = 𝑖 ) )
117 113 115 116 syl2an ( ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ∧ 𝑖 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ) → ( ( 𝑚 ↑ 2 ) = ( 𝑖 ↑ 2 ) ↔ 𝑚 = 𝑖 ) )
118 117 a1i ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ∧ 𝑖 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ) → ( ( 𝑚 ↑ 2 ) = ( 𝑖 ↑ 2 ) ↔ 𝑚 = 𝑖 ) ) )
119 111 118 dom2lem ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) : ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) –1-1→ ( 1 ... ( ⌊ ‘ 𝑥 ) ) )
120 f1f1orn ( ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) : ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) –1-1→ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) : ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) –1-1-onto→ ran ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) )
121 119 120 syl ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) : ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) –1-1-onto→ ran ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) )
122 oveq1 ( 𝑚 = 𝑖 → ( 𝑚 ↑ 2 ) = ( 𝑖 ↑ 2 ) )
123 122 72 73 fvmpt3i ( 𝑖 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) → ( ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) ‘ 𝑖 ) = ( 𝑖 ↑ 2 ) )
124 123 adantl ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑖 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ) → ( ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) ‘ 𝑖 ) = ( 𝑖 ↑ 2 ) )
125 f1f ( ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) : ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) –1-1→ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) : ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ⟶ ( 1 ... ( ⌊ ‘ 𝑥 ) ) )
126 frn ( ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) : ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ⟶ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → ran ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝑥 ) ) )
127 119 125 126 3syl ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ran ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝑥 ) ) )
128 127 sselda ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ran ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) ) → 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) )
129 1re 1 ∈ ℝ
130 0re 0 ∈ ℝ
131 129 130 ifcli if ( ( √ ‘ 𝑘 ) ∈ ℕ , 1 , 0 ) ∈ ℝ
132 rerpdivcl ( ( if ( ( √ ‘ 𝑘 ) ∈ ℕ , 1 , 0 ) ∈ ℝ ∧ ( √ ‘ 𝑘 ) ∈ ℝ+ ) → ( if ( ( √ ‘ 𝑘 ) ∈ ℕ , 1 , 0 ) / ( √ ‘ 𝑘 ) ) ∈ ℝ )
133 131 55 132 sylancr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( if ( ( √ ‘ 𝑘 ) ∈ ℕ , 1 , 0 ) / ( √ ‘ 𝑘 ) ) ∈ ℝ )
134 133 recnd ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( if ( ( √ ‘ 𝑘 ) ∈ ℕ , 1 , 0 ) / ( √ ‘ 𝑘 ) ) ∈ ℂ )
135 128 134 syldan ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ran ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) ) → ( if ( ( √ ‘ 𝑘 ) ∈ ℕ , 1 , 0 ) / ( √ ‘ 𝑘 ) ) ∈ ℂ )
136 89 135 eqeltrrd ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ran ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) ) → ( 1 / ( √ ‘ 𝑘 ) ) ∈ ℂ )
137 92 60 121 124 136 fsumf1o ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑘 ∈ ran ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) ( 1 / ( √ ‘ 𝑘 ) ) = Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ( 1 / ( √ ‘ ( 𝑖 ↑ 2 ) ) ) )
138 90 137 eqtrd ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑘 ∈ ran ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) ( if ( ( √ ‘ 𝑘 ) ∈ ℕ , 1 , 0 ) / ( √ ‘ 𝑘 ) ) = Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ( 1 / ( √ ‘ ( 𝑖 ↑ 2 ) ) ) )
139 eldif ( 𝑘 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∖ ran ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) ) ↔ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ ¬ 𝑘 ∈ ran ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) ) )
140 50 ad2antrl ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ ( √ ‘ 𝑘 ) ∈ ℕ ) ) → 𝑘 ∈ ℕ )
141 140 nncnd ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ ( √ ‘ 𝑘 ) ∈ ℕ ) ) → 𝑘 ∈ ℂ )
142 141 sqsqrtd ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ ( √ ‘ 𝑘 ) ∈ ℕ ) ) → ( ( √ ‘ 𝑘 ) ↑ 2 ) = 𝑘 )
143 simprr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ ( √ ‘ 𝑘 ) ∈ ℕ ) ) → ( √ ‘ 𝑘 ) ∈ ℕ )
144 fznnfl ( 𝑥 ∈ ℝ → ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ↔ ( 𝑘 ∈ ℕ ∧ 𝑘𝑥 ) ) )
145 103 144 syl ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ↔ ( 𝑘 ∈ ℕ ∧ 𝑘𝑥 ) ) )
146 145 simplbda ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑘𝑥 )
147 146 adantrr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ ( √ ‘ 𝑘 ) ∈ ℕ ) ) → 𝑘𝑥 )
148 140 nnrpd ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ ( √ ‘ 𝑘 ) ∈ ℕ ) ) → 𝑘 ∈ ℝ+ )
149 148 rprege0d ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ ( √ ‘ 𝑘 ) ∈ ℕ ) ) → ( 𝑘 ∈ ℝ ∧ 0 ≤ 𝑘 ) )
150 35 adantr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ ( √ ‘ 𝑘 ) ∈ ℕ ) ) → 𝑥 ∈ ℝ+ )
151 150 rprege0d ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ ( √ ‘ 𝑘 ) ∈ ℕ ) ) → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
152 sqrtle ( ( ( 𝑘 ∈ ℝ ∧ 0 ≤ 𝑘 ) ∧ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) ) → ( 𝑘𝑥 ↔ ( √ ‘ 𝑘 ) ≤ ( √ ‘ 𝑥 ) ) )
153 149 151 152 syl2anc ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ ( √ ‘ 𝑘 ) ∈ ℕ ) ) → ( 𝑘𝑥 ↔ ( √ ‘ 𝑘 ) ≤ ( √ ‘ 𝑥 ) ) )
154 147 153 mpbid ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ ( √ ‘ 𝑘 ) ∈ ℕ ) ) → ( √ ‘ 𝑘 ) ≤ ( √ ‘ 𝑥 ) )
155 68 adantr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ ( √ ‘ 𝑘 ) ∈ ℕ ) ) → ( √ ‘ 𝑥 ) ∈ ℝ+ )
156 155 rpred ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ ( √ ‘ 𝑘 ) ∈ ℕ ) ) → ( √ ‘ 𝑥 ) ∈ ℝ )
157 fznnfl ( ( √ ‘ 𝑥 ) ∈ ℝ → ( ( √ ‘ 𝑘 ) ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↔ ( ( √ ‘ 𝑘 ) ∈ ℕ ∧ ( √ ‘ 𝑘 ) ≤ ( √ ‘ 𝑥 ) ) ) )
158 156 157 syl ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ ( √ ‘ 𝑘 ) ∈ ℕ ) ) → ( ( √ ‘ 𝑘 ) ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↔ ( ( √ ‘ 𝑘 ) ∈ ℕ ∧ ( √ ‘ 𝑘 ) ≤ ( √ ‘ 𝑥 ) ) ) )
159 143 154 158 mpbir2and ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ ( √ ‘ 𝑘 ) ∈ ℕ ) ) → ( √ ‘ 𝑘 ) ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) )
160 142 140 eqeltrd ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ ( √ ‘ 𝑘 ) ∈ ℕ ) ) → ( ( √ ‘ 𝑘 ) ↑ 2 ) ∈ ℕ )
161 oveq1 ( 𝑚 = ( √ ‘ 𝑘 ) → ( 𝑚 ↑ 2 ) = ( ( √ ‘ 𝑘 ) ↑ 2 ) )
162 72 161 elrnmpt1s ( ( ( √ ‘ 𝑘 ) ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ∧ ( ( √ ‘ 𝑘 ) ↑ 2 ) ∈ ℕ ) → ( ( √ ‘ 𝑘 ) ↑ 2 ) ∈ ran ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) )
163 159 160 162 syl2anc ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ ( √ ‘ 𝑘 ) ∈ ℕ ) ) → ( ( √ ‘ 𝑘 ) ↑ 2 ) ∈ ran ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) )
164 142 163 eqeltrrd ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ ( √ ‘ 𝑘 ) ∈ ℕ ) ) → 𝑘 ∈ ran ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) )
165 164 expr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( √ ‘ 𝑘 ) ∈ ℕ → 𝑘 ∈ ran ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) ) )
166 165 con3d ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ¬ 𝑘 ∈ ran ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) → ¬ ( √ ‘ 𝑘 ) ∈ ℕ ) )
167 166 impr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ ¬ 𝑘 ∈ ran ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) ) ) → ¬ ( √ ‘ 𝑘 ) ∈ ℕ )
168 139 167 sylan2b ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∖ ran ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) ) ) → ¬ ( √ ‘ 𝑘 ) ∈ ℕ )
169 168 iffalsed ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∖ ran ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) ) ) → if ( ( √ ‘ 𝑘 ) ∈ ℕ , 1 , 0 ) = 0 )
170 169 oveq1d ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∖ ran ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) ) ) → ( if ( ( √ ‘ 𝑘 ) ∈ ℕ , 1 , 0 ) / ( √ ‘ 𝑘 ) ) = ( 0 / ( √ ‘ 𝑘 ) ) )
171 eldifi ( 𝑘 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∖ ran ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) ) → 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) )
172 171 55 sylan2 ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∖ ran ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) ) ) → ( √ ‘ 𝑘 ) ∈ ℝ+ )
173 172 rpcnne0d ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∖ ran ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) ) ) → ( ( √ ‘ 𝑘 ) ∈ ℂ ∧ ( √ ‘ 𝑘 ) ≠ 0 ) )
174 div0 ( ( ( √ ‘ 𝑘 ) ∈ ℂ ∧ ( √ ‘ 𝑘 ) ≠ 0 ) → ( 0 / ( √ ‘ 𝑘 ) ) = 0 )
175 173 174 syl ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∖ ran ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) ) ) → ( 0 / ( √ ‘ 𝑘 ) ) = 0 )
176 170 175 eqtrd ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∖ ran ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) ) ) → ( if ( ( √ ‘ 𝑘 ) ∈ ℕ , 1 , 0 ) / ( √ ‘ 𝑘 ) ) = 0 )
177 127 135 176 47 fsumss ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑘 ∈ ran ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ↦ ( 𝑚 ↑ 2 ) ) ( if ( ( √ ‘ 𝑘 ) ∈ ℕ , 1 , 0 ) / ( √ ‘ 𝑘 ) ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( if ( ( √ ‘ 𝑘 ) ∈ ℕ , 1 , 0 ) / ( √ ‘ 𝑘 ) ) )
178 62 nnrpd ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑖 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ) → 𝑖 ∈ ℝ+ )
179 178 rprege0d ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑖 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ) → ( 𝑖 ∈ ℝ ∧ 0 ≤ 𝑖 ) )
180 sqrtsq ( ( 𝑖 ∈ ℝ ∧ 0 ≤ 𝑖 ) → ( √ ‘ ( 𝑖 ↑ 2 ) ) = 𝑖 )
181 179 180 syl ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑖 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ) → ( √ ‘ ( 𝑖 ↑ 2 ) ) = 𝑖 )
182 181 oveq2d ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑖 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ) → ( 1 / ( √ ‘ ( 𝑖 ↑ 2 ) ) ) = ( 1 / 𝑖 ) )
183 182 sumeq2dv ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ( 1 / ( √ ‘ ( 𝑖 ↑ 2 ) ) ) = Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ( 1 / 𝑖 ) )
184 138 177 183 3eqtr3d ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( if ( ( √ ‘ 𝑘 ) ∈ ℕ , 1 , 0 ) / ( √ ‘ 𝑘 ) ) = Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ( 1 / 𝑖 ) )
185 131 a1i ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → if ( ( √ ‘ 𝑘 ) ∈ ℕ , 1 , 0 ) ∈ ℝ )
186 3 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑁 ∈ ℕ )
187 8 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑋𝐷 )
188 9 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℝ )
189 1 2 186 4 5 6 7 187 188 53 dchrisum0flb ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → if ( ( √ ‘ 𝑘 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹𝑘 ) )
190 185 52 55 189 lediv1dd ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( if ( ( √ ‘ 𝑘 ) ∈ ℕ , 1 , 0 ) / ( √ ‘ 𝑘 ) ) ≤ ( ( 𝐹𝑘 ) / ( √ ‘ 𝑘 ) ) )
191 47 133 56 190 fsumle ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( if ( ( √ ‘ 𝑘 ) ∈ ℕ , 1 , 0 ) / ( √ ‘ 𝑘 ) ) ≤ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝐹𝑘 ) / ( √ ‘ 𝑘 ) ) )
192 184 191 eqbrtrrd ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑥 ) ) ) ( 1 / 𝑖 ) ≤ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝐹𝑘 ) / ( √ ‘ 𝑘 ) ) )
193 30 64 57 71 192 letrd ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( log ‘ 𝑥 ) / 2 ) ≤ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝐹𝑘 ) / ( √ ‘ 𝑘 ) ) )
194 57 leabsd ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝐹𝑘 ) / ( √ ‘ 𝑘 ) ) ≤ ( abs ‘ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝐹𝑘 ) / ( √ ‘ 𝑘 ) ) ) )
195 30 57 59 193 194 letrd ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( log ‘ 𝑥 ) / 2 ) ≤ ( abs ‘ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝐹𝑘 ) / ( √ ‘ 𝑘 ) ) ) )
196 46 195 eqbrtrd ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( ( log ‘ 𝑥 ) / 2 ) ) ≤ ( abs ‘ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝐹𝑘 ) / ( √ ‘ 𝑘 ) ) ) )
197 27 10 29 21 196 o1le ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) / 2 ) ) ∈ 𝑂(1) )
198 15 21 26 197 o1mul2 ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( 2 · ( ( log ‘ 𝑥 ) / 2 ) ) ) ∈ 𝑂(1) )
199 19 198 eqeltrrd ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ 𝑂(1) )
200 11 199 mto ¬ 𝜑