Metamath Proof Explorer


Theorem dchrisum0

Description: The sum sum_ n e. NN , X ( n ) / n is nonzero for all non-principal Dirichlet characters (i.e. the assumption X e. W is contradictory). This is the key result that allows us to eliminate the conditionals from dchrmusum2 and dchrvmasumif . Lemma 9.4.4 of Shapiro, p. 382. (Contributed by Mario Carneiro, 12-May-2016)

Ref Expression
Hypotheses rpvmasum.z 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
rpvmasum.l 𝐿 = ( ℤRHom ‘ 𝑍 )
rpvmasum.a ( 𝜑𝑁 ∈ ℕ )
rpvmasum2.g 𝐺 = ( DChr ‘ 𝑁 )
rpvmasum2.d 𝐷 = ( Base ‘ 𝐺 )
rpvmasum2.1 1 = ( 0g𝐺 )
rpvmasum2.w 𝑊 = { 𝑦 ∈ ( 𝐷 ∖ { 1 } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) = 0 }
dchrisum0.b ( 𝜑𝑋𝑊 )
Assertion dchrisum0 ¬ 𝜑

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 rpvmasum2.w 𝑊 = { 𝑦 ∈ ( 𝐷 ∖ { 1 } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) = 0 }
8 dchrisum0.b ( 𝜑𝑋𝑊 )
9 eqid ( 𝑏 ∈ ℕ ↦ Σ 𝑦 ∈ { 𝑖 ∈ ℕ ∣ 𝑖𝑏 } ( 𝑋 ‘ ( 𝐿𝑦 ) ) ) = ( 𝑏 ∈ ℕ ↦ Σ 𝑦 ∈ { 𝑖 ∈ ℕ ∣ 𝑖𝑏 } ( 𝑋 ‘ ( 𝐿𝑦 ) ) )
10 7 ssrab3 𝑊 ⊆ ( 𝐷 ∖ { 1 } )
11 difss ( 𝐷 ∖ { 1 } ) ⊆ 𝐷
12 10 11 sstri 𝑊𝐷
13 12 8 sselid ( 𝜑𝑋𝐷 )
14 1 2 3 4 5 6 7 8 dchrisum0re ( 𝜑𝑋 : ( Base ‘ 𝑍 ) ⟶ ℝ )
15 fveq2 ( 𝑘 = ( 𝑚 · 𝑑 ) → ( √ ‘ 𝑘 ) = ( √ ‘ ( 𝑚 · 𝑑 ) ) )
16 15 oveq2d ( 𝑘 = ( 𝑚 · 𝑑 ) → ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ 𝑘 ) ) = ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) )
17 rpre ( 𝑥 ∈ ℝ+𝑥 ∈ ℝ )
18 17 adantl ( ( 𝜑𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ )
19 13 ad3antrrr ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ { 𝑖 ∈ ℕ ∣ 𝑖𝑘 } ) → 𝑋𝐷 )
20 elrabi ( 𝑚 ∈ { 𝑖 ∈ ℕ ∣ 𝑖𝑘 } → 𝑚 ∈ ℕ )
21 20 nnzd ( 𝑚 ∈ { 𝑖 ∈ ℕ ∣ 𝑖𝑘 } → 𝑚 ∈ ℤ )
22 21 adantl ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ { 𝑖 ∈ ℕ ∣ 𝑖𝑘 } ) → 𝑚 ∈ ℤ )
23 4 1 5 2 19 22 dchrzrhcl ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ { 𝑖 ∈ ℕ ∣ 𝑖𝑘 } ) → ( 𝑋 ‘ ( 𝐿𝑚 ) ) ∈ ℂ )
24 elfznn ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑘 ∈ ℕ )
25 24 adantl ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑘 ∈ ℕ )
26 25 nnrpd ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑘 ∈ ℝ+ )
27 26 rpsqrtcld ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( √ ‘ 𝑘 ) ∈ ℝ+ )
28 27 rpcnd ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( √ ‘ 𝑘 ) ∈ ℂ )
29 28 adantr ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ { 𝑖 ∈ ℕ ∣ 𝑖𝑘 } ) → ( √ ‘ 𝑘 ) ∈ ℂ )
30 27 rpne0d ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( √ ‘ 𝑘 ) ≠ 0 )
31 30 adantr ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ { 𝑖 ∈ ℕ ∣ 𝑖𝑘 } ) → ( √ ‘ 𝑘 ) ≠ 0 )
32 23 29 31 divcld ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ { 𝑖 ∈ ℕ ∣ 𝑖𝑘 } ) → ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ 𝑘 ) ) ∈ ℂ )
33 32 anasss ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑚 ∈ { 𝑖 ∈ ℕ ∣ 𝑖𝑘 } ) ) → ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ 𝑘 ) ) ∈ ℂ )
34 16 18 33 dvdsflsumcom ( ( 𝜑𝑥 ∈ ℝ+ ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ { 𝑖 ∈ ℕ ∣ 𝑖𝑘 } ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ 𝑘 ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) )
35 1 2 3 4 5 6 9 dchrisum0fval ( 𝑘 ∈ ℕ → ( ( 𝑏 ∈ ℕ ↦ Σ 𝑦 ∈ { 𝑖 ∈ ℕ ∣ 𝑖𝑏 } ( 𝑋 ‘ ( 𝐿𝑦 ) ) ) ‘ 𝑘 ) = Σ 𝑚 ∈ { 𝑖 ∈ ℕ ∣ 𝑖𝑘 } ( 𝑋 ‘ ( 𝐿𝑚 ) ) )
36 25 35 syl ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑏 ∈ ℕ ↦ Σ 𝑦 ∈ { 𝑖 ∈ ℕ ∣ 𝑖𝑏 } ( 𝑋 ‘ ( 𝐿𝑦 ) ) ) ‘ 𝑘 ) = Σ 𝑚 ∈ { 𝑖 ∈ ℕ ∣ 𝑖𝑘 } ( 𝑋 ‘ ( 𝐿𝑚 ) ) )
37 36 oveq1d ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑏 ∈ ℕ ↦ Σ 𝑦 ∈ { 𝑖 ∈ ℕ ∣ 𝑖𝑏 } ( 𝑋 ‘ ( 𝐿𝑦 ) ) ) ‘ 𝑘 ) / ( √ ‘ 𝑘 ) ) = ( Σ 𝑚 ∈ { 𝑖 ∈ ℕ ∣ 𝑖𝑘 } ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ 𝑘 ) ) )
38 fzfid ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ... 𝑘 ) ∈ Fin )
39 dvdsssfz1 ( 𝑘 ∈ ℕ → { 𝑖 ∈ ℕ ∣ 𝑖𝑘 } ⊆ ( 1 ... 𝑘 ) )
40 25 39 syl ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → { 𝑖 ∈ ℕ ∣ 𝑖𝑘 } ⊆ ( 1 ... 𝑘 ) )
41 38 40 ssfid ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → { 𝑖 ∈ ℕ ∣ 𝑖𝑘 } ∈ Fin )
42 41 28 23 30 fsumdivc ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑚 ∈ { 𝑖 ∈ ℕ ∣ 𝑖𝑘 } ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ 𝑘 ) ) = Σ 𝑚 ∈ { 𝑖 ∈ ℕ ∣ 𝑖𝑘 } ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ 𝑘 ) ) )
43 37 42 eqtrd ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑏 ∈ ℕ ↦ Σ 𝑦 ∈ { 𝑖 ∈ ℕ ∣ 𝑖𝑏 } ( 𝑋 ‘ ( 𝐿𝑦 ) ) ) ‘ 𝑘 ) / ( √ ‘ 𝑘 ) ) = Σ 𝑚 ∈ { 𝑖 ∈ ℕ ∣ 𝑖𝑘 } ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ 𝑘 ) ) )
44 43 sumeq2dv ( ( 𝜑𝑥 ∈ ℝ+ ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑏 ∈ ℕ ↦ Σ 𝑦 ∈ { 𝑖 ∈ ℕ ∣ 𝑖𝑏 } ( 𝑋 ‘ ( 𝐿𝑦 ) ) ) ‘ 𝑘 ) / ( √ ‘ 𝑘 ) ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ { 𝑖 ∈ ℕ ∣ 𝑖𝑘 } ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ 𝑘 ) ) )
45 rprege0 ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
46 45 adantl ( ( 𝜑𝑥 ∈ ℝ+ ) → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
47 resqrtth ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) → ( ( √ ‘ 𝑥 ) ↑ 2 ) = 𝑥 )
48 46 47 syl ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( √ ‘ 𝑥 ) ↑ 2 ) = 𝑥 )
49 48 fveq2d ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ⌊ ‘ ( ( √ ‘ 𝑥 ) ↑ 2 ) ) = ( ⌊ ‘ 𝑥 ) )
50 49 oveq2d ( ( 𝜑𝑥 ∈ ℝ+ ) → ( 1 ... ( ⌊ ‘ ( ( √ ‘ 𝑥 ) ↑ 2 ) ) ) = ( 1 ... ( ⌊ ‘ 𝑥 ) ) )
51 48 fvoveq1d ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ⌊ ‘ ( ( ( √ ‘ 𝑥 ) ↑ 2 ) / 𝑚 ) ) = ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) )
52 51 oveq2d ( ( 𝜑𝑥 ∈ ℝ+ ) → ( 1 ... ( ⌊ ‘ ( ( ( √ ‘ 𝑥 ) ↑ 2 ) / 𝑚 ) ) ) = ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) )
53 52 sumeq1d ( ( 𝜑𝑥 ∈ ℝ+ ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( ( √ ‘ 𝑥 ) ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) )
54 53 adantr ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( √ ‘ 𝑥 ) ↑ 2 ) ) ) ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( ( √ ‘ 𝑥 ) ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) )
55 50 54 sumeq12dv ( ( 𝜑𝑥 ∈ ℝ+ ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( √ ‘ 𝑥 ) ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( ( √ ‘ 𝑥 ) ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) )
56 34 44 55 3eqtr4d ( ( 𝜑𝑥 ∈ ℝ+ ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑏 ∈ ℕ ↦ Σ 𝑦 ∈ { 𝑖 ∈ ℕ ∣ 𝑖𝑏 } ( 𝑋 ‘ ( 𝐿𝑦 ) ) ) ‘ 𝑘 ) / ( √ ‘ 𝑘 ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( √ ‘ 𝑥 ) ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( ( √ ‘ 𝑥 ) ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) )
57 56 mpteq2dva ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑏 ∈ ℕ ↦ Σ 𝑦 ∈ { 𝑖 ∈ ℕ ∣ 𝑖𝑏 } ( 𝑋 ‘ ( 𝐿𝑦 ) ) ) ‘ 𝑘 ) / ( √ ‘ 𝑘 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( √ ‘ 𝑥 ) ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( ( √ ‘ 𝑥 ) ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) ) )
58 rpsqrtcl ( 𝑥 ∈ ℝ+ → ( √ ‘ 𝑥 ) ∈ ℝ+ )
59 58 adantl ( ( 𝜑𝑥 ∈ ℝ+ ) → ( √ ‘ 𝑥 ) ∈ ℝ+ )
60 eqidd ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( √ ‘ 𝑥 ) ) = ( 𝑥 ∈ ℝ+ ↦ ( √ ‘ 𝑥 ) ) )
61 eqidd ( 𝜑 → ( 𝑧 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑧 ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) ) = ( 𝑧 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑧 ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) ) )
62 oveq1 ( 𝑧 = ( √ ‘ 𝑥 ) → ( 𝑧 ↑ 2 ) = ( ( √ ‘ 𝑥 ) ↑ 2 ) )
63 62 fveq2d ( 𝑧 = ( √ ‘ 𝑥 ) → ( ⌊ ‘ ( 𝑧 ↑ 2 ) ) = ( ⌊ ‘ ( ( √ ‘ 𝑥 ) ↑ 2 ) ) )
64 63 oveq2d ( 𝑧 = ( √ ‘ 𝑥 ) → ( 1 ... ( ⌊ ‘ ( 𝑧 ↑ 2 ) ) ) = ( 1 ... ( ⌊ ‘ ( ( √ ‘ 𝑥 ) ↑ 2 ) ) ) )
65 62 fvoveq1d ( 𝑧 = ( √ ‘ 𝑥 ) → ( ⌊ ‘ ( ( 𝑧 ↑ 2 ) / 𝑚 ) ) = ( ⌊ ‘ ( ( ( √ ‘ 𝑥 ) ↑ 2 ) / 𝑚 ) ) )
66 65 oveq2d ( 𝑧 = ( √ ‘ 𝑥 ) → ( 1 ... ( ⌊ ‘ ( ( 𝑧 ↑ 2 ) / 𝑚 ) ) ) = ( 1 ... ( ⌊ ‘ ( ( ( √ ‘ 𝑥 ) ↑ 2 ) / 𝑚 ) ) ) )
67 66 sumeq1d ( 𝑧 = ( √ ‘ 𝑥 ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑧 ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( ( √ ‘ 𝑥 ) ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) )
68 67 adantr ( ( 𝑧 = ( √ ‘ 𝑥 ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 ↑ 2 ) ) ) ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑧 ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( ( √ ‘ 𝑥 ) ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) )
69 64 68 sumeq12dv ( 𝑧 = ( √ ‘ 𝑥 ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑧 ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( √ ‘ 𝑥 ) ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( ( √ ‘ 𝑥 ) ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) )
70 59 60 61 69 fmptco ( 𝜑 → ( ( 𝑧 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑧 ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) ) ∘ ( 𝑥 ∈ ℝ+ ↦ ( √ ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( √ ‘ 𝑥 ) ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( ( √ ‘ 𝑥 ) ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) ) )
71 57 70 eqtr4d ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑏 ∈ ℕ ↦ Σ 𝑦 ∈ { 𝑖 ∈ ℕ ∣ 𝑖𝑏 } ( 𝑋 ‘ ( 𝐿𝑦 ) ) ) ‘ 𝑘 ) / ( √ ‘ 𝑘 ) ) ) = ( ( 𝑧 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑧 ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) ) ∘ ( 𝑥 ∈ ℝ+ ↦ ( √ ‘ 𝑥 ) ) ) )
72 eqid ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / ( √ ‘ 𝑎 ) ) ) = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / ( √ ‘ 𝑎 ) ) )
73 1 2 3 4 5 6 7 8 72 dchrisum0lema ( 𝜑 → ∃ 𝑡𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / ( √ ‘ 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / ( √ ‘ 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / ( √ ‘ 𝑦 ) ) ) )
74 3 adantr ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / ( √ ‘ 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / ( √ ‘ 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / ( √ ‘ 𝑦 ) ) ) ) ) → 𝑁 ∈ ℕ )
75 8 adantr ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / ( √ ‘ 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / ( √ ‘ 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / ( √ ‘ 𝑦 ) ) ) ) ) → 𝑋𝑊 )
76 simprl ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / ( √ ‘ 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / ( √ ‘ 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / ( √ ‘ 𝑦 ) ) ) ) ) → 𝑐 ∈ ( 0 [,) +∞ ) )
77 simprrl ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / ( √ ‘ 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / ( √ ‘ 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / ( √ ‘ 𝑦 ) ) ) ) ) → seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / ( √ ‘ 𝑎 ) ) ) ) ⇝ 𝑡 )
78 simprrr ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / ( √ ‘ 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / ( √ ‘ 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / ( √ ‘ 𝑦 ) ) ) ) ) → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / ( √ ‘ 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / ( √ ‘ 𝑦 ) ) )
79 1 2 74 4 5 6 7 75 72 76 77 78 dchrisum0lem3 ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / ( √ ‘ 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / ( √ ‘ 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / ( √ ‘ 𝑦 ) ) ) ) ) → ( 𝑧 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑧 ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) ) ∈ 𝑂(1) )
80 79 rexlimdvaa ( 𝜑 → ( ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / ( √ ‘ 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / ( √ ‘ 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / ( √ ‘ 𝑦 ) ) ) → ( 𝑧 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑧 ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) ) ∈ 𝑂(1) ) )
81 80 exlimdv ( 𝜑 → ( ∃ 𝑡𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / ( √ ‘ 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / ( √ ‘ 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / ( √ ‘ 𝑦 ) ) ) → ( 𝑧 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑧 ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) ) ∈ 𝑂(1) ) )
82 73 81 mpd ( 𝜑 → ( 𝑧 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑧 ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) ) ∈ 𝑂(1) )
83 o1f ( ( 𝑧 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑧 ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) ) ∈ 𝑂(1) → ( 𝑧 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑧 ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) ) : dom ( 𝑧 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑧 ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) ) ⟶ ℂ )
84 82 83 syl ( 𝜑 → ( 𝑧 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑧 ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) ) : dom ( 𝑧 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑧 ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) ) ⟶ ℂ )
85 sumex Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑧 ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) ∈ V
86 eqid ( 𝑧 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑧 ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) ) = ( 𝑧 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑧 ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) )
87 85 86 dmmpti dom ( 𝑧 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑧 ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) ) = ℝ+
88 87 feq2i ( ( 𝑧 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑧 ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) ) : dom ( 𝑧 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑧 ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) ) ⟶ ℂ ↔ ( 𝑧 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑧 ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) ) : ℝ+ ⟶ ℂ )
89 84 88 sylib ( 𝜑 → ( 𝑧 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑧 ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) ) : ℝ+ ⟶ ℂ )
90 rpssre + ⊆ ℝ
91 90 a1i ( 𝜑 → ℝ+ ⊆ ℝ )
92 resqcl ( 𝑡 ∈ ℝ → ( 𝑡 ↑ 2 ) ∈ ℝ )
93 0red ( ( ( 𝜑𝑡 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ+ ∧ ( 𝑡 ↑ 2 ) ≤ 𝑥 ) ) → 0 ∈ ℝ )
94 simplr ( ( ( 𝜑𝑡 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ+ ∧ ( 𝑡 ↑ 2 ) ≤ 𝑥 ) ) → 𝑡 ∈ ℝ )
95 simplrr ( ( ( ( 𝜑𝑡 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ+ ∧ ( 𝑡 ↑ 2 ) ≤ 𝑥 ) ) ∧ 0 ≤ 𝑡 ) → ( 𝑡 ↑ 2 ) ≤ 𝑥 )
96 45 ad2antrl ( ( ( 𝜑𝑡 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ+ ∧ ( 𝑡 ↑ 2 ) ≤ 𝑥 ) ) → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
97 96 adantr ( ( ( ( 𝜑𝑡 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ+ ∧ ( 𝑡 ↑ 2 ) ≤ 𝑥 ) ) ∧ 0 ≤ 𝑡 ) → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
98 97 47 syl ( ( ( ( 𝜑𝑡 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ+ ∧ ( 𝑡 ↑ 2 ) ≤ 𝑥 ) ) ∧ 0 ≤ 𝑡 ) → ( ( √ ‘ 𝑥 ) ↑ 2 ) = 𝑥 )
99 95 98 breqtrrd ( ( ( ( 𝜑𝑡 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ+ ∧ ( 𝑡 ↑ 2 ) ≤ 𝑥 ) ) ∧ 0 ≤ 𝑡 ) → ( 𝑡 ↑ 2 ) ≤ ( ( √ ‘ 𝑥 ) ↑ 2 ) )
100 94 adantr ( ( ( ( 𝜑𝑡 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ+ ∧ ( 𝑡 ↑ 2 ) ≤ 𝑥 ) ) ∧ 0 ≤ 𝑡 ) → 𝑡 ∈ ℝ )
101 59 rpred ( ( 𝜑𝑥 ∈ ℝ+ ) → ( √ ‘ 𝑥 ) ∈ ℝ )
102 101 ad2ant2r ( ( ( 𝜑𝑡 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ+ ∧ ( 𝑡 ↑ 2 ) ≤ 𝑥 ) ) → ( √ ‘ 𝑥 ) ∈ ℝ )
103 102 adantr ( ( ( ( 𝜑𝑡 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ+ ∧ ( 𝑡 ↑ 2 ) ≤ 𝑥 ) ) ∧ 0 ≤ 𝑡 ) → ( √ ‘ 𝑥 ) ∈ ℝ )
104 simpr ( ( ( ( 𝜑𝑡 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ+ ∧ ( 𝑡 ↑ 2 ) ≤ 𝑥 ) ) ∧ 0 ≤ 𝑡 ) → 0 ≤ 𝑡 )
105 sqrtge0 ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) → 0 ≤ ( √ ‘ 𝑥 ) )
106 96 105 syl ( ( ( 𝜑𝑡 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ+ ∧ ( 𝑡 ↑ 2 ) ≤ 𝑥 ) ) → 0 ≤ ( √ ‘ 𝑥 ) )
107 106 adantr ( ( ( ( 𝜑𝑡 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ+ ∧ ( 𝑡 ↑ 2 ) ≤ 𝑥 ) ) ∧ 0 ≤ 𝑡 ) → 0 ≤ ( √ ‘ 𝑥 ) )
108 100 103 104 107 le2sqd ( ( ( ( 𝜑𝑡 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ+ ∧ ( 𝑡 ↑ 2 ) ≤ 𝑥 ) ) ∧ 0 ≤ 𝑡 ) → ( 𝑡 ≤ ( √ ‘ 𝑥 ) ↔ ( 𝑡 ↑ 2 ) ≤ ( ( √ ‘ 𝑥 ) ↑ 2 ) ) )
109 99 108 mpbird ( ( ( ( 𝜑𝑡 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ+ ∧ ( 𝑡 ↑ 2 ) ≤ 𝑥 ) ) ∧ 0 ≤ 𝑡 ) → 𝑡 ≤ ( √ ‘ 𝑥 ) )
110 94 adantr ( ( ( ( 𝜑𝑡 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ+ ∧ ( 𝑡 ↑ 2 ) ≤ 𝑥 ) ) ∧ 𝑡 ≤ 0 ) → 𝑡 ∈ ℝ )
111 0red ( ( ( ( 𝜑𝑡 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ+ ∧ ( 𝑡 ↑ 2 ) ≤ 𝑥 ) ) ∧ 𝑡 ≤ 0 ) → 0 ∈ ℝ )
112 102 adantr ( ( ( ( 𝜑𝑡 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ+ ∧ ( 𝑡 ↑ 2 ) ≤ 𝑥 ) ) ∧ 𝑡 ≤ 0 ) → ( √ ‘ 𝑥 ) ∈ ℝ )
113 simpr ( ( ( ( 𝜑𝑡 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ+ ∧ ( 𝑡 ↑ 2 ) ≤ 𝑥 ) ) ∧ 𝑡 ≤ 0 ) → 𝑡 ≤ 0 )
114 106 adantr ( ( ( ( 𝜑𝑡 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ+ ∧ ( 𝑡 ↑ 2 ) ≤ 𝑥 ) ) ∧ 𝑡 ≤ 0 ) → 0 ≤ ( √ ‘ 𝑥 ) )
115 110 111 112 113 114 letrd ( ( ( ( 𝜑𝑡 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ+ ∧ ( 𝑡 ↑ 2 ) ≤ 𝑥 ) ) ∧ 𝑡 ≤ 0 ) → 𝑡 ≤ ( √ ‘ 𝑥 ) )
116 93 94 109 115 lecasei ( ( ( 𝜑𝑡 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ+ ∧ ( 𝑡 ↑ 2 ) ≤ 𝑥 ) ) → 𝑡 ≤ ( √ ‘ 𝑥 ) )
117 116 expr ( ( ( 𝜑𝑡 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝑡 ↑ 2 ) ≤ 𝑥𝑡 ≤ ( √ ‘ 𝑥 ) ) )
118 117 ralrimiva ( ( 𝜑𝑡 ∈ ℝ ) → ∀ 𝑥 ∈ ℝ+ ( ( 𝑡 ↑ 2 ) ≤ 𝑥𝑡 ≤ ( √ ‘ 𝑥 ) ) )
119 breq1 ( 𝑐 = ( 𝑡 ↑ 2 ) → ( 𝑐𝑥 ↔ ( 𝑡 ↑ 2 ) ≤ 𝑥 ) )
120 119 rspceaimv ( ( ( 𝑡 ↑ 2 ) ∈ ℝ ∧ ∀ 𝑥 ∈ ℝ+ ( ( 𝑡 ↑ 2 ) ≤ 𝑥𝑡 ≤ ( √ ‘ 𝑥 ) ) ) → ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ ℝ+ ( 𝑐𝑥𝑡 ≤ ( √ ‘ 𝑥 ) ) )
121 92 118 120 syl2an2 ( ( 𝜑𝑡 ∈ ℝ ) → ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ ℝ+ ( 𝑐𝑥𝑡 ≤ ( √ ‘ 𝑥 ) ) )
122 89 82 59 91 121 o1compt ( 𝜑 → ( ( 𝑧 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑧 ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) ) ∘ ( 𝑥 ∈ ℝ+ ↦ ( √ ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
123 71 122 eqeltrd ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑏 ∈ ℕ ↦ Σ 𝑦 ∈ { 𝑖 ∈ ℕ ∣ 𝑖𝑏 } ( 𝑋 ‘ ( 𝐿𝑦 ) ) ) ‘ 𝑘 ) / ( √ ‘ 𝑘 ) ) ) ∈ 𝑂(1) )
124 1 2 3 4 5 6 9 13 14 123 dchrisum0fno1 ¬ 𝜑