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 |
⊢ ¬ 𝜑 |