Proof of Theorem dchrisum0flblem2
| Step | Hyp | Ref
| Expression |
| 1 | | breq1 5146 |
. . 3
⊢ (1 =
if((√‘𝐴) ∈
ℕ, 1, 0) → (1 ≤ ((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) ↔ if((√‘𝐴) ∈ ℕ, 1, 0) ≤
((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))))) |
| 2 | | breq1 5146 |
. . 3
⊢ (0 =
if((√‘𝐴) ∈
ℕ, 1, 0) → (0 ≤ ((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) ↔ if((√‘𝐴) ∈ ℕ, 1, 0) ≤
((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))))) |
| 3 | | 1t1e1 12428 |
. . . 4
⊢ (1
· 1) = 1 |
| 4 | | dchrisum0flb.2 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑃 ∈ ℙ) |
| 5 | 4 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 𝑃 ∈
ℙ) |
| 6 | | nnq 13004 |
. . . . . . . . . . . . . . 15
⊢
((√‘𝐴)
∈ ℕ → (√‘𝐴) ∈ ℚ) |
| 7 | 6 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘𝐴) ∈
ℚ) |
| 8 | | nnne0 12300 |
. . . . . . . . . . . . . . 15
⊢
((√‘𝐴)
∈ ℕ → (√‘𝐴) ≠ 0) |
| 9 | 8 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘𝐴) ≠
0) |
| 10 | | 2z 12649 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℤ |
| 11 | 10 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 2
∈ ℤ) |
| 12 | | pcexp 16897 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧
((√‘𝐴) ∈
ℚ ∧ (√‘𝐴) ≠ 0) ∧ 2 ∈ ℤ) →
(𝑃 pCnt
((√‘𝐴)↑2))
= (2 · (𝑃 pCnt
(√‘𝐴)))) |
| 13 | 5, 7, 9, 11, 12 | syl121anc 1377 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃 pCnt ((√‘𝐴)↑2)) = (2 · (𝑃 pCnt (√‘𝐴)))) |
| 14 | | dchrisum0flb.1 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ∈
(ℤ≥‘2)) |
| 15 | | eluz2nn 12924 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈
(ℤ≥‘2) → 𝐴 ∈ ℕ) |
| 16 | 14, 15 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐴 ∈ ℕ) |
| 17 | 16 | nncnd 12282 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ∈ ℂ) |
| 18 | 17 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 𝐴 ∈
ℂ) |
| 19 | 18 | sqsqrtd 15478 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
((√‘𝐴)↑2)
= 𝐴) |
| 20 | 19 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃 pCnt ((√‘𝐴)↑2)) = (𝑃 pCnt 𝐴)) |
| 21 | | 2cnd 12344 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 2
∈ ℂ) |
| 22 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘𝐴) ∈
ℕ) |
| 23 | 5, 22 | pccld 16888 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃 pCnt (√‘𝐴)) ∈
ℕ0) |
| 24 | 23 | nn0cnd 12589 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃 pCnt (√‘𝐴)) ∈
ℂ) |
| 25 | 21, 24 | mulcomd 11282 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (2
· (𝑃 pCnt
(√‘𝐴))) =
((𝑃 pCnt
(√‘𝐴)) ·
2)) |
| 26 | 13, 20, 25 | 3eqtr3rd 2786 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → ((𝑃 pCnt (√‘𝐴)) · 2) = (𝑃 pCnt 𝐴)) |
| 27 | 26 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃↑((𝑃 pCnt (√‘𝐴)) · 2)) = (𝑃↑(𝑃 pCnt 𝐴))) |
| 28 | | prmnn 16711 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
| 29 | 5, 28 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 𝑃 ∈
ℕ) |
| 30 | 29 | nncnd 12282 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 𝑃 ∈
ℂ) |
| 31 | | 2nn0 12543 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℕ0 |
| 32 | 31 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 2
∈ ℕ0) |
| 33 | 30, 32, 23 | expmuld 14189 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃↑((𝑃 pCnt (√‘𝐴)) · 2)) = ((𝑃↑(𝑃 pCnt (√‘𝐴)))↑2)) |
| 34 | 27, 33 | eqtr3d 2779 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃↑(𝑃 pCnt 𝐴)) = ((𝑃↑(𝑃 pCnt (√‘𝐴)))↑2)) |
| 35 | 34 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘(𝑃↑(𝑃 pCnt 𝐴))) = (√‘((𝑃↑(𝑃 pCnt (√‘𝐴)))↑2))) |
| 36 | 29, 23 | nnexpcld 14284 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃↑(𝑃 pCnt (√‘𝐴))) ∈ ℕ) |
| 37 | 36 | nnrpd 13075 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃↑(𝑃 pCnt (√‘𝐴))) ∈
ℝ+) |
| 38 | 37 | rprege0d 13084 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → ((𝑃↑(𝑃 pCnt (√‘𝐴))) ∈ ℝ ∧ 0 ≤ (𝑃↑(𝑃 pCnt (√‘𝐴))))) |
| 39 | | sqrtsq 15308 |
. . . . . . . . . 10
⊢ (((𝑃↑(𝑃 pCnt (√‘𝐴))) ∈ ℝ ∧ 0 ≤ (𝑃↑(𝑃 pCnt (√‘𝐴)))) → (√‘((𝑃↑(𝑃 pCnt (√‘𝐴)))↑2)) = (𝑃↑(𝑃 pCnt (√‘𝐴)))) |
| 40 | 38, 39 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘((𝑃↑(𝑃 pCnt (√‘𝐴)))↑2)) = (𝑃↑(𝑃 pCnt (√‘𝐴)))) |
| 41 | 35, 40 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘(𝑃↑(𝑃 pCnt 𝐴))) = (𝑃↑(𝑃 pCnt (√‘𝐴)))) |
| 42 | 41, 36 | eqeltrd 2841 |
. . . . . . 7
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ) |
| 43 | 42 | iftrued 4533 |
. . . . . 6
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0) =
1) |
| 44 | | rpvmasum.z |
. . . . . . . 8
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
| 45 | | rpvmasum.l |
. . . . . . . 8
⊢ 𝐿 = (ℤRHom‘𝑍) |
| 46 | | rpvmasum.a |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 47 | | rpvmasum2.g |
. . . . . . . 8
⊢ 𝐺 = (DChr‘𝑁) |
| 48 | | rpvmasum2.d |
. . . . . . . 8
⊢ 𝐷 = (Base‘𝐺) |
| 49 | | rpvmasum2.1 |
. . . . . . . 8
⊢ 1 =
(0g‘𝐺) |
| 50 | | dchrisum0f.f |
. . . . . . . 8
⊢ 𝐹 = (𝑏 ∈ ℕ ↦ Σ𝑣 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏} (𝑋‘(𝐿‘𝑣))) |
| 51 | | dchrisum0f.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ 𝐷) |
| 52 | | dchrisum0flb.r |
. . . . . . . 8
⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℝ) |
| 53 | 4, 16 | pccld 16888 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 pCnt 𝐴) ∈
ℕ0) |
| 54 | 44, 45, 46, 47, 48, 49, 50, 51, 52, 4, 53 | dchrisum0flblem1 27552 |
. . . . . . 7
⊢ (𝜑 → if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0) ≤ (𝐹‘(𝑃↑(𝑃 pCnt 𝐴)))) |
| 55 | 54 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0) ≤ (𝐹‘(𝑃↑(𝑃 pCnt 𝐴)))) |
| 56 | 43, 55 | eqbrtrrd 5167 |
. . . . 5
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 1 ≤
(𝐹‘(𝑃↑(𝑃 pCnt 𝐴)))) |
| 57 | | pcdvds 16902 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐴) |
| 58 | 4, 16, 57 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐴) |
| 59 | 4, 28 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑃 ∈ ℕ) |
| 60 | 59, 53 | nnexpcld 14284 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℕ) |
| 61 | | nndivdvds 16299 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ ∧ (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℕ) → ((𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐴 ↔ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ)) |
| 62 | 16, 60, 61 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐴 ↔ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ)) |
| 63 | 58, 62 | mpbid 232 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ) |
| 64 | 63 | nnzd 12640 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ ℤ) |
| 65 | 64 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ ℤ) |
| 66 | 16 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 𝐴 ∈
ℕ) |
| 67 | 66 | nnrpd 13075 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 𝐴 ∈
ℝ+) |
| 68 | 67 | rprege0d 13084 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝐴 ∈ ℝ ∧ 0 ≤
𝐴)) |
| 69 | 60 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℕ) |
| 70 | 69 | nnrpd 13075 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃↑(𝑃 pCnt 𝐴)) ∈
ℝ+) |
| 71 | | sqrtdiv 15304 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℝ+) →
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = ((√‘𝐴) / (√‘(𝑃↑(𝑃 pCnt 𝐴))))) |
| 72 | 68, 70, 71 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = ((√‘𝐴) / (√‘(𝑃↑(𝑃 pCnt 𝐴))))) |
| 73 | | nnz 12634 |
. . . . . . . . . . 11
⊢
((√‘𝐴)
∈ ℕ → (√‘𝐴) ∈ ℤ) |
| 74 | | znq 12994 |
. . . . . . . . . . 11
⊢
(((√‘𝐴)
∈ ℤ ∧ (√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ) →
((√‘𝐴) /
(√‘(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℚ) |
| 75 | 73, 42, 74 | syl2an2 686 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
((√‘𝐴) /
(√‘(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℚ) |
| 76 | 72, 75 | eqeltrd 2841 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℚ) |
| 77 | | zsqrtelqelz 16795 |
. . . . . . . . 9
⊢ (((𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ ℤ ∧
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℚ) →
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℤ) |
| 78 | 65, 76, 77 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℤ) |
| 79 | 63 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ) |
| 80 | 79 | nnrpd 13075 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈
ℝ+) |
| 81 | 80 | sqrtgt0d 15451 |
. . . . . . . 8
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 0 <
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) |
| 82 | | elnnz 12623 |
. . . . . . . 8
⊢
((√‘(𝐴 /
(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ ↔
((√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℤ ∧ 0 <
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
| 83 | 78, 81, 82 | sylanbrc 583 |
. . . . . . 7
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ) |
| 84 | 83 | iftrued 4533 |
. . . . . 6
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
if((√‘(𝐴 /
(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) =
1) |
| 85 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) → (√‘𝑦) = (√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) |
| 86 | 85 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) → ((√‘𝑦) ∈ ℕ ↔
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ)) |
| 87 | 86 | ifbid 4549 |
. . . . . . . . 9
⊢ (𝑦 = (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) → if((√‘𝑦) ∈ ℕ, 1, 0) =
if((√‘(𝐴 /
(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0)) |
| 88 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑦 = (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) → (𝐹‘𝑦) = (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) |
| 89 | 87, 88 | breq12d 5156 |
. . . . . . . 8
⊢ (𝑦 = (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) → (if((√‘𝑦) ∈ ℕ, 1, 0) ≤
(𝐹‘𝑦) ↔ if((√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) ≤ (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
| 90 | | dchrisum0flb.4 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑦 ∈ (1..^𝐴)if((√‘𝑦) ∈ ℕ, 1, 0) ≤ (𝐹‘𝑦)) |
| 91 | | nnuz 12921 |
. . . . . . . . . 10
⊢ ℕ =
(ℤ≥‘1) |
| 92 | 63, 91 | eleqtrdi 2851 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈
(ℤ≥‘1)) |
| 93 | 16 | nnzd 12640 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℤ) |
| 94 | 59 | nnred 12281 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈ ℝ) |
| 95 | | dchrisum0flb.3 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 ∥ 𝐴) |
| 96 | | pcelnn 16908 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) → ((𝑃 pCnt 𝐴) ∈ ℕ ↔ 𝑃 ∥ 𝐴)) |
| 97 | 4, 16, 96 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑃 pCnt 𝐴) ∈ ℕ ↔ 𝑃 ∥ 𝐴)) |
| 98 | 95, 97 | mpbird 257 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑃 pCnt 𝐴) ∈ ℕ) |
| 99 | | prmuz2 16733 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
| 100 | | eluz2gt1 12962 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈
(ℤ≥‘2) → 1 < 𝑃) |
| 101 | 4, 99, 100 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 < 𝑃) |
| 102 | | expgt1 14141 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℝ ∧ (𝑃 pCnt 𝐴) ∈ ℕ ∧ 1 < 𝑃) → 1 < (𝑃↑(𝑃 pCnt 𝐴))) |
| 103 | 94, 98, 101, 102 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 < (𝑃↑(𝑃 pCnt 𝐴))) |
| 104 | | 1red 11262 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℝ) |
| 105 | | 0lt1 11785 |
. . . . . . . . . . . . 13
⊢ 0 <
1 |
| 106 | 105 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < 1) |
| 107 | 60 | nnred 12281 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℝ) |
| 108 | 60 | nngt0d 12315 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < (𝑃↑(𝑃 pCnt 𝐴))) |
| 109 | 16 | nnred 12281 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 110 | 16 | nngt0d 12315 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < 𝐴) |
| 111 | | ltdiv2 12154 |
. . . . . . . . . . . 12
⊢ (((1
∈ ℝ ∧ 0 < 1) ∧ ((𝑃↑(𝑃 pCnt 𝐴)) ∈ ℝ ∧ 0 < (𝑃↑(𝑃 pCnt 𝐴))) ∧ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) → (1 < (𝑃↑(𝑃 pCnt 𝐴)) ↔ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) < (𝐴 / 1))) |
| 112 | 104, 106,
107, 108, 109, 110, 111 | syl222anc 1388 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 < (𝑃↑(𝑃 pCnt 𝐴)) ↔ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) < (𝐴 / 1))) |
| 113 | 103, 112 | mpbid 232 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) < (𝐴 / 1)) |
| 114 | 17 | div1d 12035 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 / 1) = 𝐴) |
| 115 | 113, 114 | breqtrd 5169 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) < 𝐴) |
| 116 | | elfzo2 13702 |
. . . . . . . . 9
⊢ ((𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ (1..^𝐴) ↔ ((𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ (ℤ≥‘1)
∧ 𝐴 ∈ ℤ
∧ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) < 𝐴)) |
| 117 | 92, 93, 115, 116 | syl3anbrc 1344 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ (1..^𝐴)) |
| 118 | 89, 90, 117 | rspcdva 3623 |
. . . . . . 7
⊢ (𝜑 → if((√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) ≤ (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) |
| 119 | 118 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
if((√‘(𝐴 /
(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) ≤ (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) |
| 120 | 84, 119 | eqbrtrrd 5167 |
. . . . 5
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 1 ≤
(𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) |
| 121 | | 1re 11261 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
| 122 | | 0le1 11786 |
. . . . . . . 8
⊢ 0 ≤
1 |
| 123 | 121, 122 | pm3.2i 470 |
. . . . . . 7
⊢ (1 ∈
ℝ ∧ 0 ≤ 1) |
| 124 | 123 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (1
∈ ℝ ∧ 0 ≤ 1)) |
| 125 | 44, 45, 46, 47, 48, 49, 50, 51, 52 | dchrisum0ff 27551 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:ℕ⟶ℝ) |
| 126 | 125, 60 | ffvelcdmd 7105 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℝ) |
| 127 | 126 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℝ) |
| 128 | 125, 63 | ffvelcdmd 7105 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℝ) |
| 129 | 128 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℝ) |
| 130 | | lemul12a 12125 |
. . . . . 6
⊢ ((((1
∈ ℝ ∧ 0 ≤ 1) ∧ (𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℝ) ∧ ((1 ∈ ℝ
∧ 0 ≤ 1) ∧ (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℝ)) → ((1 ≤ (𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) ∧ 1 ≤ (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) → (1 · 1) ≤ ((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))))) |
| 131 | 124, 127,
124, 129, 130 | syl22anc 839 |
. . . . 5
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → ((1
≤ (𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) ∧ 1 ≤ (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) → (1 · 1) ≤ ((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))))) |
| 132 | 56, 120, 131 | mp2and 699 |
. . . 4
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (1
· 1) ≤ ((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
| 133 | 3, 132 | eqbrtrrid 5179 |
. . 3
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 1 ≤
((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
| 134 | | 0red 11264 |
. . . . . 6
⊢ (𝜑 → 0 ∈
ℝ) |
| 135 | | 0re 11263 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
| 136 | 121, 135 | ifcli 4573 |
. . . . . . 7
⊢
if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0) ∈
ℝ |
| 137 | 136 | a1i 11 |
. . . . . 6
⊢ (𝜑 → if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0) ∈
ℝ) |
| 138 | | breq2 5147 |
. . . . . . . 8
⊢ (1 =
if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0) → (0 ≤ 1
↔ 0 ≤ if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0))) |
| 139 | | breq2 5147 |
. . . . . . . 8
⊢ (0 =
if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0) → (0 ≤ 0
↔ 0 ≤ if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0))) |
| 140 | | 0le0 12367 |
. . . . . . . 8
⊢ 0 ≤
0 |
| 141 | 138, 139,
122, 140 | keephyp 4597 |
. . . . . . 7
⊢ 0 ≤
if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0) |
| 142 | 141 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 0 ≤
if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0)) |
| 143 | 134, 137,
126, 142, 54 | letrd 11418 |
. . . . 5
⊢ (𝜑 → 0 ≤ (𝐹‘(𝑃↑(𝑃 pCnt 𝐴)))) |
| 144 | 121, 135 | ifcli 4573 |
. . . . . . 7
⊢
if((√‘(𝐴
/ (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) ∈
ℝ |
| 145 | 144 | a1i 11 |
. . . . . 6
⊢ (𝜑 → if((√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) ∈
ℝ) |
| 146 | | breq2 5147 |
. . . . . . . 8
⊢ (1 =
if((√‘(𝐴 /
(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) → (0 ≤ 1
↔ 0 ≤ if((√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1,
0))) |
| 147 | | breq2 5147 |
. . . . . . . 8
⊢ (0 =
if((√‘(𝐴 /
(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) → (0 ≤ 0
↔ 0 ≤ if((√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1,
0))) |
| 148 | 146, 147,
122, 140 | keephyp 4597 |
. . . . . . 7
⊢ 0 ≤
if((√‘(𝐴 /
(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) |
| 149 | 148 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 0 ≤
if((√‘(𝐴 /
(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0)) |
| 150 | 134, 145,
128, 149, 118 | letrd 11418 |
. . . . 5
⊢ (𝜑 → 0 ≤ (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) |
| 151 | 126, 128,
143, 150 | mulge0d 11840 |
. . . 4
⊢ (𝜑 → 0 ≤ ((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
| 152 | 151 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ ¬ (√‘𝐴) ∈ ℕ) → 0 ≤
((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
| 153 | 1, 2, 133, 152 | ifbothda 4564 |
. 2
⊢ (𝜑 → if((√‘𝐴) ∈ ℕ, 1, 0) ≤
((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
| 154 | 60 | nncnd 12282 |
. . . . 5
⊢ (𝜑 → (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℂ) |
| 155 | 60 | nnne0d 12316 |
. . . . 5
⊢ (𝜑 → (𝑃↑(𝑃 pCnt 𝐴)) ≠ 0) |
| 156 | 17, 154, 155 | divcan2d 12045 |
. . . 4
⊢ (𝜑 → ((𝑃↑(𝑃 pCnt 𝐴)) · (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 𝐴) |
| 157 | 156 | fveq2d 6910 |
. . 3
⊢ (𝜑 → (𝐹‘((𝑃↑(𝑃 pCnt 𝐴)) · (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) = (𝐹‘𝐴)) |
| 158 | | pcndvds2 16906 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) → ¬
𝑃 ∥ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) |
| 159 | 4, 16, 158 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → ¬ 𝑃 ∥ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) |
| 160 | | coprm 16748 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ ℤ) → (¬ 𝑃 ∥ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ↔ (𝑃 gcd (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 1)) |
| 161 | 4, 64, 160 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (¬ 𝑃 ∥ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ↔ (𝑃 gcd (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 1)) |
| 162 | 159, 161 | mpbid 232 |
. . . . 5
⊢ (𝜑 → (𝑃 gcd (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 1) |
| 163 | | prmz 16712 |
. . . . . . 7
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
| 164 | 4, 163 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈ ℤ) |
| 165 | | rpexp1i 16760 |
. . . . . 6
⊢ ((𝑃 ∈ ℤ ∧ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ ℤ ∧ (𝑃 pCnt 𝐴) ∈ ℕ0) → ((𝑃 gcd (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 1 → ((𝑃↑(𝑃 pCnt 𝐴)) gcd (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 1)) |
| 166 | 164, 64, 53, 165 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → ((𝑃 gcd (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 1 → ((𝑃↑(𝑃 pCnt 𝐴)) gcd (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 1)) |
| 167 | 162, 166 | mpd 15 |
. . . 4
⊢ (𝜑 → ((𝑃↑(𝑃 pCnt 𝐴)) gcd (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 1) |
| 168 | 44, 45, 46, 47, 48, 49, 50, 51, 60, 63, 167 | dchrisum0fmul 27550 |
. . 3
⊢ (𝜑 → (𝐹‘((𝑃↑(𝑃 pCnt 𝐴)) · (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) = ((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
| 169 | 157, 168 | eqtr3d 2779 |
. 2
⊢ (𝜑 → (𝐹‘𝐴) = ((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
| 170 | 153, 169 | breqtrrd 5171 |
1
⊢ (𝜑 → if((√‘𝐴) ∈ ℕ, 1, 0) ≤
(𝐹‘𝐴)) |