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 ffvelcdm ⊢ ( ( 𝐹 : ℕ ⟶ ℝ ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
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 biimtrid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 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 ⊢ ¬ 𝜑