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

Metamath Proof Explorer

Theorem dchrisum0flblem2

Description: Lemma for dchrisum0flb . Induction over relatively prime factors, with the prime power case handled in dchrisum0flblem1 . (Contributed by Mario Carneiro, 5-May-2016) Replace reference to OLD theorem. (Revised by Wolf Lammen, 8-Sep-2020)

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.1 ⊢ ( 𝜑 → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
dchrisum0flb.2 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
dchrisum0flb.3 ⊢ ( 𝜑 → 𝑃 ∥ 𝐴 )
dchrisum0flb.4 ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 1 ..^ 𝐴 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) )
Assertion dchrisum0flblem2 ( 𝜑 → 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.1 ⊢ ( 𝜑 → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
11 dchrisum0flb.2 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
12 dchrisum0flb.3 ⊢ ( 𝜑 → 𝑃 ∥ 𝐴 )
13 dchrisum0flb.4 ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 1 ..^ 𝐴 ) if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) )
14 breq1 ⊢ ( 1 = if ( ( √ ‘ 𝐴 ) ∈ ℕ , 1 , 0 ) → ( 1 ≤ ( ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) · ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) ↔ if ( ( √ ‘ 𝐴 ) ∈ ℕ , 1 , 0 ) ≤ ( ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) · ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) ) )
15 breq1 ⊢ ( 0 = if ( ( √ ‘ 𝐴 ) ∈ ℕ , 1 , 0 ) → ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) · ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) ↔ if ( ( √ ‘ 𝐴 ) ∈ ℕ , 1 , 0 ) ≤ ( ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) · ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) ) )
16 1t1e1 ⊢ ( 1 · 1 ) = 1
17 11 adantr ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → 𝑃 ∈ ℙ )
18 nnq ⊢ ( ( √ ‘ 𝐴 ) ∈ ℕ → ( √ ‘ 𝐴 ) ∈ ℚ )
19 18 adantl ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( √ ‘ 𝐴 ) ∈ ℚ )
20 nnne0 ⊢ ( ( √ ‘ 𝐴 ) ∈ ℕ → ( √ ‘ 𝐴 ) ≠ 0 )
21 20 adantl ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( √ ‘ 𝐴 ) ≠ 0 )
22 2z ⊢ 2 ∈ ℤ
23 22 a1i ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → 2 ∈ ℤ )
24 pcexp ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( √ ‘ 𝐴 ) ∈ ℚ ∧ ( √ ‘ 𝐴 ) ≠ 0 ) ∧ 2 ∈ ℤ ) → ( 𝑃 pCnt ( ( √ ‘ 𝐴 ) ↑ 2 ) ) = ( 2 · ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ) )
25 17 19 21 23 24 syl121anc ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 𝑃 pCnt ( ( √ ‘ 𝐴 ) ↑ 2 ) ) = ( 2 · ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ) )
26 eluz2nn ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℕ )
27 10 26 syl ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
28 27 nncnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
29 28 adantr ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → 𝐴 ∈ ℂ )
30 29 sqsqrtd ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( ( √ ‘ 𝐴 ) ↑ 2 ) = 𝐴 )
31 30 oveq2d ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 𝑃 pCnt ( ( √ ‘ 𝐴 ) ↑ 2 ) ) = ( 𝑃 pCnt 𝐴 ) )
32 2cnd ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → 2 ∈ ℂ )
33 simpr ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( √ ‘ 𝐴 ) ∈ ℕ )
34 17 33 pccld ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ∈ ℕ0 )
35 34 nn0cnd ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ∈ ℂ )
36 32 35 mulcomd ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 2 · ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ) = ( ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) · 2 ) )
37 25 31 36 3eqtr3rd ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) · 2 ) = ( 𝑃 pCnt 𝐴 ) )
38 37 oveq2d ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 𝑃 ↑ ( ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) · 2 ) ) = ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) )
39 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
40 17 39 syl ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → 𝑃 ∈ ℕ )
41 40 nncnd ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → 𝑃 ∈ ℂ )
42 2nn0 ⊢ 2 ∈ ℕ0
43 42 a1i ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → 2 ∈ ℕ0 )
44 41 43 34 expmuld ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 𝑃 ↑ ( ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) · 2 ) ) = ( ( 𝑃 ↑ ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ) ↑ 2 ) )
45 38 44 eqtr3d ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) = ( ( 𝑃 ↑ ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ) ↑ 2 ) )
46 45 fveq2d ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) = ( √ ‘ ( ( 𝑃 ↑ ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ) ↑ 2 ) ) )
47 40 34 nnexpcld ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 𝑃 ↑ ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ) ∈ ℕ )
48 47 nnrpd ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 𝑃 ↑ ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ) ∈ ℝ+ )
49 48 rprege0d ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑃 ↑ ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ) ∈ ℝ ∧ 0 ≤ ( 𝑃 ↑ ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ) ) )
50 sqrtsq ⊢ ( ( ( 𝑃 ↑ ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ) ∈ ℝ ∧ 0 ≤ ( 𝑃 ↑ ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ) ) → ( √ ‘ ( ( 𝑃 ↑ ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ) ↑ 2 ) ) = ( 𝑃 ↑ ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ) )
51 49 50 syl ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( √ ‘ ( ( 𝑃 ↑ ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ) ↑ 2 ) ) = ( 𝑃 ↑ ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ) )
52 46 51 eqtrd ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) = ( 𝑃 ↑ ( 𝑃 pCnt ( √ ‘ 𝐴 ) ) ) )
53 52 47 eqeltrd ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℕ )
54 53 iftrued ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → if ( ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℕ , 1 , 0 ) = 1 )
55 11 27 pccld ⊢ ( 𝜑 → ( 𝑃 pCnt 𝐴 ) ∈ ℕ0 )
56 1 2 3 4 5 6 7 8 9 11 55 dchrisum0flblem1 ⊢ ( 𝜑 → if ( ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) )
57 56 adantr ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → if ( ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) )
58 54 57 eqbrtrrd ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → 1 ≤ ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) )
59 pcdvds ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ 𝐴 )
60 11 27 59 syl2anc ⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ 𝐴 )
61 11 39 syl ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
62 61 55 nnexpcld ⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∈ ℕ )
63 nndivdvds ⊢ ( ( 𝐴 ∈ ℕ ∧ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∈ ℕ ) → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ 𝐴 ↔ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℕ ) )
64 27 62 63 syl2anc ⊢ ( 𝜑 → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ 𝐴 ↔ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℕ ) )
65 60 64 mpbid ⊢ ( 𝜑 → ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℕ )
66 65 nnzd ⊢ ( 𝜑 → ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℤ )
67 66 adantr ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℤ )
68 27 adantr ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → 𝐴 ∈ ℕ )
69 68 nnrpd ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → 𝐴 ∈ ℝ+ )
70 69 rprege0d ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) )
71 62 adantr ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∈ ℕ )
72 71 nnrpd ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∈ ℝ+ )
73 sqrtdiv ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∈ ℝ+ ) → ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) = ( ( √ ‘ 𝐴 ) / ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) )
74 70 72 73 syl2anc ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) = ( ( √ ‘ 𝐴 ) / ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) )
75 nnz ⊢ ( ( √ ‘ 𝐴 ) ∈ ℕ → ( √ ‘ 𝐴 ) ∈ ℤ )
76 znq ⊢ ( ( ( √ ‘ 𝐴 ) ∈ ℤ ∧ ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℕ ) → ( ( √ ‘ 𝐴 ) / ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℚ )
77 75 53 76 syl2an2 ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( ( √ ‘ 𝐴 ) / ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℚ )
78 74 77 eqeltrd ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℚ )
79 zsqrtelqelz ⊢ ( ( ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℤ ∧ ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℚ ) → ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℤ )
80 67 78 79 syl2anc ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℤ )
81 65 adantr ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℕ )
82 81 nnrpd ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℝ+ )
83 82 sqrtgt0d ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → 0 < ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) )
84 elnnz ⊢ ( ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℕ ↔ ( ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℤ ∧ 0 < ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) )
85 80 83 84 sylanbrc ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℕ )
86 85 iftrued ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → if ( ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℕ , 1 , 0 ) = 1 )
87 fveq2 ⊢ ( 𝑦 = ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) → ( √ ‘ 𝑦 ) = ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) )
88 87 eleq1d ⊢ ( 𝑦 = ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) → ( ( √ ‘ 𝑦 ) ∈ ℕ ↔ ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℕ ) )
89 88 ifbid ⊢ ( 𝑦 = ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) → if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) = if ( ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℕ , 1 , 0 ) )
90 fveq2 ⊢ ( 𝑦 = ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) )
91 89 90 breq12d ⊢ ( 𝑦 = ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) → ( if ( ( √ ‘ 𝑦 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝑦 ) ↔ if ( ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) )
92 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
93 65 92 eleqtrdi ⊢ ( 𝜑 → ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ( ℤ≥ ‘ 1 ) )
94 27 nnzd ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
95 61 nnred ⊢ ( 𝜑 → 𝑃 ∈ ℝ )
96 pcelnn ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ( ( 𝑃 pCnt 𝐴 ) ∈ ℕ ↔ 𝑃 ∥ 𝐴 ) )
97 11 27 96 syl2anc ⊢ ( 𝜑 → ( ( 𝑃 pCnt 𝐴 ) ∈ ℕ ↔ 𝑃 ∥ 𝐴 ) )
98 12 97 mpbird ⊢ ( 𝜑 → ( 𝑃 pCnt 𝐴 ) ∈ ℕ )
99 prmuz2 ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
100 eluz2gt1 ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝑃 )
101 11 99 100 3syl ⊢ ( 𝜑 → 1 < 𝑃 )
102 expgt1 ⊢ ( ( 𝑃 ∈ ℝ ∧ ( 𝑃 pCnt 𝐴 ) ∈ ℕ ∧ 1 < 𝑃 ) → 1 < ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) )
103 95 98 101 102 syl3anc ⊢ ( 𝜑 → 1 < ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) )
104 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
105 0lt1 ⊢ 0 < 1
106 105 a1i ⊢ ( 𝜑 → 0 < 1 )
107 62 nnred ⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∈ ℝ )
108 62 nngt0d ⊢ ( 𝜑 → 0 < ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) )
109 27 nnred ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
110 27 nngt0d ⊢ ( 𝜑 → 0 < 𝐴 )
111 ltdiv2 ⊢ ( ( ( 1 ∈ ℝ ∧ 0 < 1 ) ∧ ( ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∈ ℝ ∧ 0 < ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → ( 1 < ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ↔ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) < ( 𝐴 / 1 ) ) )
112 104 106 107 108 109 110 111 syl222anc ⊢ ( 𝜑 → ( 1 < ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ↔ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) < ( 𝐴 / 1 ) ) )
113 103 112 mpbid ⊢ ( 𝜑 → ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) < ( 𝐴 / 1 ) )
114 28 div1d ⊢ ( 𝜑 → ( 𝐴 / 1 ) = 𝐴 )
115 113 114 breqtrd ⊢ ( 𝜑 → ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) < 𝐴 )
116 elfzo2 ⊢ ( ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ( 1 ..^ 𝐴 ) ↔ ( ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ( ℤ≥ ‘ 1 ) ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) < 𝐴 ) )
117 93 94 115 116 syl3anbrc ⊢ ( 𝜑 → ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ( 1 ..^ 𝐴 ) )
118 91 13 117 rspcdva ⊢ ( 𝜑 → if ( ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) )
119 118 adantr ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → if ( ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) )
120 86 119 eqbrtrrd ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → 1 ≤ ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) )
121 1re ⊢ 1 ∈ ℝ
122 0le1 ⊢ 0 ≤ 1
123 121 122 pm3.2i ⊢ ( 1 ∈ ℝ ∧ 0 ≤ 1 )
124 123 a1i ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 1 ∈ ℝ ∧ 0 ≤ 1 ) )
125 1 2 3 4 5 6 7 8 9 dchrisum0ff ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ℝ )
126 125 62 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℝ )
127 126 adantr ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℝ )
128 125 65 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℝ )
129 128 adantr ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℝ )
130 lemul12a ⊢ ( ( ( ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ∧ ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℝ ) ∧ ( ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ∧ ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℝ ) ) → ( ( 1 ≤ ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∧ 1 ≤ ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) → ( 1 · 1 ) ≤ ( ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) · ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) ) )
131 124 127 124 129 130 syl22anc ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( ( 1 ≤ ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∧ 1 ≤ ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) → ( 1 · 1 ) ≤ ( ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) · ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) ) )
132 58 120 131 mp2and ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 1 · 1 ) ≤ ( ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) · ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) )
133 16 132 eqbrtrrid ⊢ ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → 1 ≤ ( ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) · ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) )
134 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
135 0re ⊢ 0 ∈ ℝ
136 121 135 ifcli ⊢ if ( ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℕ , 1 , 0 ) ∈ ℝ
137 136 a1i ⊢ ( 𝜑 → if ( ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℕ , 1 , 0 ) ∈ ℝ )
138 breq2 ⊢ ( 1 = if ( ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℕ , 1 , 0 ) → ( 0 ≤ 1 ↔ 0 ≤ if ( ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℕ , 1 , 0 ) ) )
139 breq2 ⊢ ( 0 = if ( ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℕ , 1 , 0 ) → ( 0 ≤ 0 ↔ 0 ≤ if ( ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℕ , 1 , 0 ) ) )
140 0le0 ⊢ 0 ≤ 0
141 138 139 122 140 keephyp ⊢ 0 ≤ if ( ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℕ , 1 , 0 )
142 141 a1i ⊢ ( 𝜑 → 0 ≤ if ( ( √ ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℕ , 1 , 0 ) )
143 134 137 126 142 56 letrd ⊢ ( 𝜑 → 0 ≤ ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) )
144 121 135 ifcli ⊢ if ( ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℕ , 1 , 0 ) ∈ ℝ
145 144 a1i ⊢ ( 𝜑 → if ( ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℕ , 1 , 0 ) ∈ ℝ )
146 breq2 ⊢ ( 1 = if ( ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℕ , 1 , 0 ) → ( 0 ≤ 1 ↔ 0 ≤ if ( ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℕ , 1 , 0 ) ) )
147 breq2 ⊢ ( 0 = if ( ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℕ , 1 , 0 ) → ( 0 ≤ 0 ↔ 0 ≤ if ( ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℕ , 1 , 0 ) ) )
148 146 147 122 140 keephyp ⊢ 0 ≤ if ( ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℕ , 1 , 0 )
149 148 a1i ⊢ ( 𝜑 → 0 ≤ if ( ( √ ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ∈ ℕ , 1 , 0 ) )
150 134 145 128 149 118 letrd ⊢ ( 𝜑 → 0 ≤ ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) )
151 126 128 143 150 mulge0d ⊢ ( 𝜑 → 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) · ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) )
152 151 adantr ⊢ ( ( 𝜑 ∧ ¬ ( √ ‘ 𝐴 ) ∈ ℕ ) → 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) · ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) )
153 14 15 133 152 ifbothda ⊢ ( 𝜑 → if ( ( √ ‘ 𝐴 ) ∈ ℕ , 1 , 0 ) ≤ ( ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) · ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) )
154 62 nncnd ⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∈ ℂ )
155 62 nnne0d ⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ≠ 0 )
156 28 154 155 divcan2d ⊢ ( 𝜑 → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) · ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) = 𝐴 )
157 156 fveq2d ⊢ ( 𝜑 → ( 𝐹 ‘ ( ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) · ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) = ( 𝐹 ‘ 𝐴 ) )
158 pcndvds2 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ¬ 𝑃 ∥ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) )
159 11 27 158 syl2anc ⊢ ( 𝜑 → ¬ 𝑃 ∥ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) )
160 coprm ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℤ ) → ( ¬ 𝑃 ∥ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ↔ ( 𝑃 gcd ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) = 1 ) )
161 11 66 160 syl2anc ⊢ ( 𝜑 → ( ¬ 𝑃 ∥ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ↔ ( 𝑃 gcd ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) = 1 ) )
162 159 161 mpbid ⊢ ( 𝜑 → ( 𝑃 gcd ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) = 1 )
163 prmz ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
164 11 163 syl ⊢ ( 𝜑 → 𝑃 ∈ ℤ )
165 rpexp1i ⊢ ( ( 𝑃 ∈ ℤ ∧ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℤ ∧ ( 𝑃 pCnt 𝐴 ) ∈ ℕ0 ) → ( ( 𝑃 gcd ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) = 1 → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) gcd ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) = 1 ) )
166 164 66 55 165 syl3anc ⊢ ( 𝜑 → ( ( 𝑃 gcd ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) = 1 → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) gcd ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) = 1 ) )
167 162 166 mpd ⊢ ( 𝜑 → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) gcd ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) = 1 )
168 1 2 3 4 5 6 7 8 62 65 167 dchrisum0fmul ⊢ ( 𝜑 → ( 𝐹 ‘ ( ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) · ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) = ( ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) · ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) )
169 157 168 eqtr3d ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = ( ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) · ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ) ) )
170 153 169 breqtrrd ⊢ ( 𝜑 → if ( ( √ ‘ 𝐴 ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ 𝐴 ) )