This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dchrisum0flb

Description: The divisor sum of a real Dirichlet character, is lower bounded by zero everywhere and one at the squares. Equation 9.4.29 of Shapiro, p. 382. (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 ‘ 𝑍 ) ⟶ ℝ )
dchrisum0flb.a ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
Assertion dchrisum0flb ( 𝜑 → if ( ( √ ‘ 𝐴 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝐴 ) )

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 dchrisum0flb.a ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
11 fveq2 ⊢ ( 𝑦 = 𝐴 → ( √ ‘ 𝑦 ) = ( √ ‘ 𝐴 ) )
12 11 eleq1d ⊢ ( 𝑦 = 𝐴 → ( ( √ ‘ 𝑦 ) ∈ ℕ ↔ ( √ ‘ 𝐴 ) ∈ ℕ ) )
13 12 ifbid ⊢ ( 𝑦 = 𝐴 → if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) = if ( ( √ ‘ 𝐴 ) ∈ ℕ , 1 , 0 ) )
14 fveq2 ⊢ ( 𝑦 = 𝐴 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐴 ) )
15 13 14 breq12d ⊢ ( 𝑦 = 𝐴 → ( if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ↔ if ( ( √ ‘ 𝐴 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝐴 ) ) )
16 oveq2 ⊢ ( 𝑘 = 1 → ( 1 ... 𝑘 ) = ( 1 ... 1 ) )
17 16 raleqdv ⊢ ( 𝑘 = 1 → ( ∀ 𝑦 ∈ ( 1 ... 𝑘 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ ( 1 ... 1 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
18 17 imbi2d ⊢ ( 𝑘 = 1 → ( ( 𝜑 → ∀ 𝑦 ∈ ( 1 ... 𝑘 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝜑 → ∀ 𝑦 ∈ ( 1 ... 1 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) )
19 oveq2 ⊢ ( 𝑘 = 𝑖 → ( 1 ... 𝑘 ) = ( 1 ... 𝑖 ) )
20 19 raleqdv ⊢ ( 𝑘 = 𝑖 → ( ∀ 𝑦 ∈ ( 1 ... 𝑘 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ ( 1 ... 𝑖 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
21 20 imbi2d ⊢ ( 𝑘 = 𝑖 → ( ( 𝜑 → ∀ 𝑦 ∈ ( 1 ... 𝑘 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝜑 → ∀ 𝑦 ∈ ( 1 ... 𝑖 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) )
22 oveq2 ⊢ ( 𝑘 = ( 𝑖 + 1 ) → ( 1 ... 𝑘 ) = ( 1 ... ( 𝑖 + 1 ) ) )
23 22 raleqdv ⊢ ( 𝑘 = ( 𝑖 + 1 ) → ( ∀ 𝑦 ∈ ( 1 ... 𝑘 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ ( 1 ... ( 𝑖 + 1 ) ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
24 23 imbi2d ⊢ ( 𝑘 = ( 𝑖 + 1 ) → ( ( 𝜑 → ∀ 𝑦 ∈ ( 1 ... 𝑘 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝜑 → ∀ 𝑦 ∈ ( 1 ... ( 𝑖 + 1 ) ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) )
25 oveq2 ⊢ ( 𝑘 = 𝐴 → ( 1 ... 𝑘 ) = ( 1 ... 𝐴 ) )
26 25 raleqdv ⊢ ( 𝑘 = 𝐴 → ( ∀ 𝑦 ∈ ( 1 ... 𝑘 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ ( 1 ... 𝐴 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
27 26 imbi2d ⊢ ( 𝑘 = 𝐴 → ( ( 𝜑 → ∀ 𝑦 ∈ ( 1 ... 𝑘 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝜑 → ∀ 𝑦 ∈ ( 1 ... 𝐴 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) )
28 2prm ⊢ 2 ∈ ℙ
29 28 a1i ⊢ ( 𝜑 → 2 ∈ ℙ )
30 0nn0 ⊢ 0 ∈ ℕ0
31 30 a1i ⊢ ( 𝜑 → 0 ∈ ℕ0 )
32 1 2 3 4 5 6 7 8 9 29 31 dchrisum0flblem1 ⊢ ( 𝜑 → if ( ( √ ‘ ( 2 ↑ 0 ) ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ ( 2 ↑ 0 ) ) )
33 elfz1eq ⊢ ( 𝑦 ∈ ( 1 ... 1 ) → 𝑦 = 1 )
34 2nn0 ⊢ 2 ∈ ℕ0
35 34 numexp0 ⊢ ( 2 ↑ 0 ) = 1
36 33 35 eqtr4di ⊢ ( 𝑦 ∈ ( 1 ... 1 ) → 𝑦 = ( 2 ↑ 0 ) )
37 36 fveq2d ⊢ ( 𝑦 ∈ ( 1 ... 1 ) → ( √ ‘ 𝑦 ) = ( √ ‘ ( 2 ↑ 0 ) ) )
38 37 eleq1d ⊢ ( 𝑦 ∈ ( 1 ... 1 ) → ( ( √ ‘ 𝑦 ) ∈ ℕ ↔ ( √ ‘ ( 2 ↑ 0 ) ) ∈ ℕ ) )
39 38 ifbid ⊢ ( 𝑦 ∈ ( 1 ... 1 ) → if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) = if ( ( √ ‘ ( 2 ↑ 0 ) ) ∈ ℕ , 1 , 0 ) )
40 36 fveq2d ⊢ ( 𝑦 ∈ ( 1 ... 1 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( 2 ↑ 0 ) ) )
41 39 40 breq12d ⊢ ( 𝑦 ∈ ( 1 ... 1 ) → ( if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ↔ if ( ( √ ‘ ( 2 ↑ 0 ) ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ ( 2 ↑ 0 ) ) ) )
42 41 biimprcd ⊢ ( if ( ( √ ‘ ( 2 ↑ 0 ) ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ ( 2 ↑ 0 ) ) → ( 𝑦 ∈ ( 1 ... 1 ) → if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
43 42 ralrimiv ⊢ ( if ( ( √ ‘ ( 2 ↑ 0 ) ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ ( 2 ↑ 0 ) ) → ∀ 𝑦 ∈ ( 1 ... 1 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) )
44 32 43 syl ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 1 ... 1 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) )
45 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → 𝑖 ∈ ℕ )
46 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
47 45 46 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → 𝑖 ∈ ( ℤ≥ ‘ 1 ) )
48 47 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ℕ ∧ ∀ 𝑦 ∈ ( 1 ... 𝑖 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) → 𝑖 ∈ ( ℤ≥ ‘ 1 ) )
49 eluzp1p1 ⊢ ( 𝑖 ∈ ( ℤ≥ ‘ 1 ) → ( 𝑖 + 1 ) ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) )
50 48 49 syl ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ℕ ∧ ∀ 𝑦 ∈ ( 1 ... 𝑖 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝑖 + 1 ) ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) )
51 df-2 ⊢ 2 = ( 1 + 1 )
52 51 fveq2i ⊢ ( ℤ≥ ‘ 2 ) = ( ℤ≥ ‘ ( 1 + 1 ) )
53 50 52 eleqtrrdi ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ℕ ∧ ∀ 𝑦 ∈ ( 1 ... 𝑖 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝑖 + 1 ) ∈ ( ℤ≥ ‘ 2 ) )
54 exprmfct ⊢ ( ( 𝑖 + 1 ) ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ ( 𝑖 + 1 ) )
55 53 54 syl ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ℕ ∧ ∀ 𝑦 ∈ ( 1 ... 𝑖 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ ( 𝑖 + 1 ) )
56 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℕ ∧ ∀ 𝑦 ∈ ( 1 ... 𝑖 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( 𝑖 + 1 ) ) ) → 𝑁 ∈ ℕ )
57 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℕ ∧ ∀ 𝑦 ∈ ( 1 ... 𝑖 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( 𝑖 + 1 ) ) ) → 𝑋 ∈ 𝐷 )
58 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℕ ∧ ∀ 𝑦 ∈ ( 1 ... 𝑖 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( 𝑖 + 1 ) ) ) → 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℝ )
59 53 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℕ ∧ ∀ 𝑦 ∈ ( 1 ... 𝑖 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( 𝑖 + 1 ) ) ) → ( 𝑖 + 1 ) ∈ ( ℤ≥ ‘ 2 ) )
60 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℕ ∧ ∀ 𝑦 ∈ ( 1 ... 𝑖 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( 𝑖 + 1 ) ) ) → 𝑝 ∈ ℙ )
61 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℕ ∧ ∀ 𝑦 ∈ ( 1 ... 𝑖 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( 𝑖 + 1 ) ) ) → 𝑝 ∥ ( 𝑖 + 1 ) )
62 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℕ ∧ ∀ 𝑦 ∈ ( 1 ... 𝑖 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( 𝑖 + 1 ) ) ) → ∀ 𝑦 ∈ ( 1 ... 𝑖 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) )
63 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℕ ∧ ∀ 𝑦 ∈ ( 1 ... 𝑖 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( 𝑖 + 1 ) ) ) → 𝑖 ∈ ℕ )
64 63 nnzd ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℕ ∧ ∀ 𝑦 ∈ ( 1 ... 𝑖 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( 𝑖 + 1 ) ) ) → 𝑖 ∈ ℤ )
65 fzval3 ⊢ ( 𝑖 ∈ ℤ → ( 1 ... 𝑖 ) = ( 1 ..^ ( 𝑖 + 1 ) ) )
66 64 65 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℕ ∧ ∀ 𝑦 ∈ ( 1 ... 𝑖 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( 𝑖 + 1 ) ) ) → ( 1 ... 𝑖 ) = ( 1 ..^ ( 𝑖 + 1 ) ) )
67 62 66 raleqtrdv ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℕ ∧ ∀ 𝑦 ∈ ( 1 ... 𝑖 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( 𝑖 + 1 ) ) ) → ∀ 𝑦 ∈ ( 1 ..^ ( 𝑖 + 1 ) ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) )
68 1 2 56 4 5 6 7 57 58 59 60 61 67 dchrisum0flblem2 ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℕ ∧ ∀ 𝑦 ∈ ( 1 ... 𝑖 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( 𝑖 + 1 ) ) ) → if ( ( √ ‘ ( 𝑖 + 1 ) ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ ( 𝑖 + 1 ) ) )
69 55 68 rexlimddv ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ℕ ∧ ∀ 𝑦 ∈ ( 1 ... 𝑖 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) → if ( ( √ ‘ ( 𝑖 + 1 ) ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ ( 𝑖 + 1 ) ) )
70 ovex ⊢ ( 𝑖 + 1 ) ∈ V
71 fveq2 ⊢ ( 𝑦 = ( 𝑖 + 1 ) → ( √ ‘ 𝑦 ) = ( √ ‘ ( 𝑖 + 1 ) ) )
72 71 eleq1d ⊢ ( 𝑦 = ( 𝑖 + 1 ) → ( ( √ ‘ 𝑦 ) ∈ ℕ ↔ ( √ ‘ ( 𝑖 + 1 ) ) ∈ ℕ ) )
73 72 ifbid ⊢ ( 𝑦 = ( 𝑖 + 1 ) → if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) = if ( ( √ ‘ ( 𝑖 + 1 ) ) ∈ ℕ , 1 , 0 ) )
74 fveq2 ⊢ ( 𝑦 = ( 𝑖 + 1 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑖 + 1 ) ) )
75 73 74 breq12d ⊢ ( 𝑦 = ( 𝑖 + 1 ) → ( if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ↔ if ( ( √ ‘ ( 𝑖 + 1 ) ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ ( 𝑖 + 1 ) ) ) )
76 70 75 ralsn ⊢ ( ∀ 𝑦 ∈ { ( 𝑖 + 1 ) } if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ↔ if ( ( √ ‘ ( 𝑖 + 1 ) ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ ( 𝑖 + 1 ) ) )
77 69 76 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ℕ ∧ ∀ 𝑦 ∈ ( 1 ... 𝑖 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) → ∀ 𝑦 ∈ { ( 𝑖 + 1 ) } if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) )
78 77 expr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( ∀ 𝑦 ∈ ( 1 ... 𝑖 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) → ∀ 𝑦 ∈ { ( 𝑖 + 1 ) } if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
79 78 ancld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( ∀ 𝑦 ∈ ( 1 ... 𝑖 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) → ( ∀ 𝑦 ∈ ( 1 ... 𝑖 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ { ( 𝑖 + 1 ) } if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) )
80 fzsuc ⊢ ( 𝑖 ∈ ( ℤ≥ ‘ 1 ) → ( 1 ... ( 𝑖 + 1 ) ) = ( ( 1 ... 𝑖 ) ∪ { ( 𝑖 + 1 ) } ) )
81 47 80 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( 1 ... ( 𝑖 + 1 ) ) = ( ( 1 ... 𝑖 ) ∪ { ( 𝑖 + 1 ) } ) )
82 81 raleqdv ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( ∀ 𝑦 ∈ ( 1 ... ( 𝑖 + 1 ) ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ ( ( 1 ... 𝑖 ) ∪ { ( 𝑖 + 1 ) } ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
83 ralunb ⊢ ( ∀ 𝑦 ∈ ( ( 1 ... 𝑖 ) ∪ { ( 𝑖 + 1 ) } ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ↔ ( ∀ 𝑦 ∈ ( 1 ... 𝑖 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ { ( 𝑖 + 1 ) } if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
84 82 83 bitrdi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( ∀ 𝑦 ∈ ( 1 ... ( 𝑖 + 1 ) ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ↔ ( ∀ 𝑦 ∈ ( 1 ... 𝑖 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ { ( 𝑖 + 1 ) } if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) )
85 79 84 sylibrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( ∀ 𝑦 ∈ ( 1 ... 𝑖 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) → ∀ 𝑦 ∈ ( 1 ... ( 𝑖 + 1 ) ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
86 85 expcom ⊢ ( 𝑖 ∈ ℕ → ( 𝜑 → ( ∀ 𝑦 ∈ ( 1 ... 𝑖 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) → ∀ 𝑦 ∈ ( 1 ... ( 𝑖 + 1 ) ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) )
87 86 a2d ⊢ ( 𝑖 ∈ ℕ → ( ( 𝜑 → ∀ 𝑦 ∈ ( 1 ... 𝑖 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) → ( 𝜑 → ∀ 𝑦 ∈ ( 1 ... ( 𝑖 + 1 ) ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) )
88 18 21 24 27 44 87 nnind ⊢ ( 𝐴 ∈ ℕ → ( 𝜑 → ∀ 𝑦 ∈ ( 1 ... 𝐴 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
89 10 88 mpcom ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 1 ... 𝐴 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) )
90 10 46 eleqtrdi ⊢ ( 𝜑 → 𝐴 ∈ ( ℤ≥ ‘ 1 ) )
91 eluzfz2 ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 1 ) → 𝐴 ∈ ( 1 ... 𝐴 ) )
92 90 91 syl ⊢ ( 𝜑 → 𝐴 ∈ ( 1 ... 𝐴 ) )
93 15 89 92 rspcdva ⊢ ( 𝜑 → if ( ( √ ‘ 𝐴 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝐴 ) )