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 ffvelrnd ( 𝜑 → ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℝ )
127 126 adantr ( ( 𝜑 ∧ ( √ ‘ 𝐴 ) ∈ ℕ ) → ( 𝐹 ‘ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) ∈ ℝ )
128 125 65 ffvelrnd ( 𝜑 → ( 𝐹 ‘ ( 𝐴 / ( 𝑃 ↑ ( 𝑃 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 ) ≤ ( 𝐹𝐴 ) )