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