Proof of Theorem dchrisum0flblem2
Step | Hyp | Ref
| Expression |
1 | | breq1 4846 |
. . 3
⊢ (1 =
if((√‘𝐴) ∈
ℕ, 1, 0) → (1 ≤ ((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) ↔ if((√‘𝐴) ∈ ℕ, 1, 0) ≤
((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))))) |
2 | | breq1 4846 |
. . 3
⊢ (0 =
if((√‘𝐴) ∈
ℕ, 1, 0) → (0 ≤ ((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) ↔ if((√‘𝐴) ∈ ℕ, 1, 0) ≤
((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))))) |
3 | | 1t1e1 11482 |
. . . 4
⊢ (1
· 1) = 1 |
4 | | dchrisum0flb.2 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑃 ∈ ℙ) |
5 | 4 | adantr 473 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 𝑃 ∈
ℙ) |
6 | | nnq 12046 |
. . . . . . . . . . . . . . 15
⊢
((√‘𝐴)
∈ ℕ → (√‘𝐴) ∈ ℚ) |
7 | 6 | adantl 474 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘𝐴) ∈
ℚ) |
8 | | nnne0 11348 |
. . . . . . . . . . . . . . 15
⊢
((√‘𝐴)
∈ ℕ → (√‘𝐴) ≠ 0) |
9 | 8 | adantl 474 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘𝐴) ≠
0) |
10 | | 2z 11699 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℤ |
11 | 10 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 2
∈ ℤ) |
12 | | pcexp 15897 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧
((√‘𝐴) ∈
ℚ ∧ (√‘𝐴) ≠ 0) ∧ 2 ∈ ℤ) →
(𝑃 pCnt
((√‘𝐴)↑2))
= (2 · (𝑃 pCnt
(√‘𝐴)))) |
13 | 5, 7, 9, 11, 12 | syl121anc 1495 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃 pCnt ((√‘𝐴)↑2)) = (2 · (𝑃 pCnt (√‘𝐴)))) |
14 | | dchrisum0flb.1 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ∈
(ℤ≥‘2)) |
15 | | eluz2nn 11970 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈
(ℤ≥‘2) → 𝐴 ∈ ℕ) |
16 | 14, 15 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐴 ∈ ℕ) |
17 | 16 | nncnd 11330 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ∈ ℂ) |
18 | 17 | adantr 473 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 𝐴 ∈
ℂ) |
19 | 18 | sqsqrtd 14519 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
((√‘𝐴)↑2)
= 𝐴) |
20 | 19 | oveq2d 6894 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃 pCnt ((√‘𝐴)↑2)) = (𝑃 pCnt 𝐴)) |
21 | | 2cnd 11391 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 2
∈ ℂ) |
22 | | simpr 478 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘𝐴) ∈
ℕ) |
23 | 5, 22 | pccld 15888 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃 pCnt (√‘𝐴)) ∈
ℕ0) |
24 | 23 | nn0cnd 11642 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃 pCnt (√‘𝐴)) ∈
ℂ) |
25 | 21, 24 | mulcomd 10350 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (2
· (𝑃 pCnt
(√‘𝐴))) =
((𝑃 pCnt
(√‘𝐴)) ·
2)) |
26 | 13, 20, 25 | 3eqtr3rd 2842 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → ((𝑃 pCnt (√‘𝐴)) · 2) = (𝑃 pCnt 𝐴)) |
27 | 26 | oveq2d 6894 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃↑((𝑃 pCnt (√‘𝐴)) · 2)) = (𝑃↑(𝑃 pCnt 𝐴))) |
28 | | prmnn 15722 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
29 | 5, 28 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 𝑃 ∈
ℕ) |
30 | 29 | nncnd 11330 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 𝑃 ∈
ℂ) |
31 | | 2nn0 11599 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℕ0 |
32 | 31 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 2
∈ ℕ0) |
33 | 30, 32, 23 | expmuld 13265 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃↑((𝑃 pCnt (√‘𝐴)) · 2)) = ((𝑃↑(𝑃 pCnt (√‘𝐴)))↑2)) |
34 | 27, 33 | eqtr3d 2835 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃↑(𝑃 pCnt 𝐴)) = ((𝑃↑(𝑃 pCnt (√‘𝐴)))↑2)) |
35 | 34 | fveq2d 6415 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘(𝑃↑(𝑃 pCnt 𝐴))) = (√‘((𝑃↑(𝑃 pCnt (√‘𝐴)))↑2))) |
36 | 29, 23 | nnexpcld 13286 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃↑(𝑃 pCnt (√‘𝐴))) ∈ ℕ) |
37 | 36 | nnrpd 12115 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃↑(𝑃 pCnt (√‘𝐴))) ∈
ℝ+) |
38 | 37 | rprege0d 12124 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → ((𝑃↑(𝑃 pCnt (√‘𝐴))) ∈ ℝ ∧ 0 ≤ (𝑃↑(𝑃 pCnt (√‘𝐴))))) |
39 | | sqrtsq 14351 |
. . . . . . . . . 10
⊢ (((𝑃↑(𝑃 pCnt (√‘𝐴))) ∈ ℝ ∧ 0 ≤ (𝑃↑(𝑃 pCnt (√‘𝐴)))) → (√‘((𝑃↑(𝑃 pCnt (√‘𝐴)))↑2)) = (𝑃↑(𝑃 pCnt (√‘𝐴)))) |
40 | 38, 39 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘((𝑃↑(𝑃 pCnt (√‘𝐴)))↑2)) = (𝑃↑(𝑃 pCnt (√‘𝐴)))) |
41 | 35, 40 | eqtrd 2833 |
. . . . . . . 8
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘(𝑃↑(𝑃 pCnt 𝐴))) = (𝑃↑(𝑃 pCnt (√‘𝐴)))) |
42 | 41, 36 | eqeltrd 2878 |
. . . . . . 7
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ) |
43 | 42 | iftrued 4285 |
. . . . . 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 15888 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 pCnt 𝐴) ∈
ℕ0) |
54 | 44, 45, 46, 47, 48, 49, 50, 51, 52, 4, 53 | dchrisum0flblem1 25549 |
. . . . . . 7
⊢ (𝜑 → if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0) ≤ (𝐹‘(𝑃↑(𝑃 pCnt 𝐴)))) |
55 | 54 | adantr 473 |
. . . . . 6
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0) ≤ (𝐹‘(𝑃↑(𝑃 pCnt 𝐴)))) |
56 | 43, 55 | eqbrtrrd 4867 |
. . . . 5
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 1 ≤
(𝐹‘(𝑃↑(𝑃 pCnt 𝐴)))) |
57 | | pcdvds 15901 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐴) |
58 | 4, 16, 57 | syl2anc 580 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐴) |
59 | 4, 28 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑃 ∈ ℕ) |
60 | 59, 53 | nnexpcld 13286 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℕ) |
61 | | nndivdvds 15328 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ ∧ (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℕ) → ((𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐴 ↔ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ)) |
62 | 16, 60, 61 | syl2anc 580 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐴 ↔ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ)) |
63 | 58, 62 | mpbid 224 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ) |
64 | 63 | nnzd 11771 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ ℤ) |
65 | 64 | adantr 473 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ ℤ) |
66 | 16 | adantr 473 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 𝐴 ∈
ℕ) |
67 | 66 | nnrpd 12115 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 𝐴 ∈
ℝ+) |
68 | 67 | rprege0d 12124 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝐴 ∈ ℝ ∧ 0 ≤
𝐴)) |
69 | 60 | adantr 473 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℕ) |
70 | 69 | nnrpd 12115 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃↑(𝑃 pCnt 𝐴)) ∈
ℝ+) |
71 | | sqrtdiv 14347 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℝ+) →
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = ((√‘𝐴) / (√‘(𝑃↑(𝑃 pCnt 𝐴))))) |
72 | 68, 70, 71 | syl2anc 580 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = ((√‘𝐴) / (√‘(𝑃↑(𝑃 pCnt 𝐴))))) |
73 | | nnz 11689 |
. . . . . . . . . . . 12
⊢
((√‘𝐴)
∈ ℕ → (√‘𝐴) ∈ ℤ) |
74 | 73 | adantl 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘𝐴) ∈
ℤ) |
75 | | znq 12037 |
. . . . . . . . . . 11
⊢
(((√‘𝐴)
∈ ℤ ∧ (√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ) →
((√‘𝐴) /
(√‘(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℚ) |
76 | 74, 42, 75 | syl2anc 580 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
((√‘𝐴) /
(√‘(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℚ) |
77 | 72, 76 | eqeltrd 2878 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℚ) |
78 | | zsqrtelqelz 15799 |
. . . . . . . . 9
⊢ (((𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ ℤ ∧
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℚ) →
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℤ) |
79 | 65, 77, 78 | syl2anc 580 |
. . . . . . . 8
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℤ) |
80 | 63 | adantr 473 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ) |
81 | 80 | nnrpd 12115 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈
ℝ+) |
82 | 81 | sqrtgt0d 14492 |
. . . . . . . 8
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 0 <
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) |
83 | | elnnz 11676 |
. . . . . . . 8
⊢
((√‘(𝐴 /
(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ ↔
((√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℤ ∧ 0 <
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
84 | 79, 82, 83 | sylanbrc 579 |
. . . . . . 7
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ) |
85 | 84 | iftrued 4285 |
. . . . . 6
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
if((√‘(𝐴 /
(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) =
1) |
86 | | fveq2 6411 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) → (√‘𝑦) = (√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) |
87 | 86 | eleq1d 2863 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) → ((√‘𝑦) ∈ ℕ ↔
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ)) |
88 | 87 | ifbid 4299 |
. . . . . . . . 9
⊢ (𝑦 = (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) → if((√‘𝑦) ∈ ℕ, 1, 0) =
if((√‘(𝐴 /
(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0)) |
89 | | fveq2 6411 |
. . . . . . . . 9
⊢ (𝑦 = (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) → (𝐹‘𝑦) = (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) |
90 | 88, 89 | breq12d 4856 |
. . . . . . . 8
⊢ (𝑦 = (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) → (if((√‘𝑦) ∈ ℕ, 1, 0) ≤
(𝐹‘𝑦) ↔ if((√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) ≤ (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
91 | | dchrisum0flb.4 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑦 ∈ (1..^𝐴)if((√‘𝑦) ∈ ℕ, 1, 0) ≤ (𝐹‘𝑦)) |
92 | | nnuz 11967 |
. . . . . . . . . 10
⊢ ℕ =
(ℤ≥‘1) |
93 | 63, 92 | syl6eleq 2888 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈
(ℤ≥‘1)) |
94 | 16 | nnzd 11771 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℤ) |
95 | 59 | nnred 11329 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈ ℝ) |
96 | | dchrisum0flb.3 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 ∥ 𝐴) |
97 | | pcelnn 15907 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) → ((𝑃 pCnt 𝐴) ∈ ℕ ↔ 𝑃 ∥ 𝐴)) |
98 | 4, 16, 97 | syl2anc 580 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑃 pCnt 𝐴) ∈ ℕ ↔ 𝑃 ∥ 𝐴)) |
99 | 96, 98 | mpbird 249 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑃 pCnt 𝐴) ∈ ℕ) |
100 | | prmuz2 15742 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
101 | | eluz2b2 12006 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈
(ℤ≥‘2) ↔ (𝑃 ∈ ℕ ∧ 1 < 𝑃)) |
102 | 101 | simprbi 491 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈
(ℤ≥‘2) → 1 < 𝑃) |
103 | 4, 100, 102 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 < 𝑃) |
104 | | expgt1 13152 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℝ ∧ (𝑃 pCnt 𝐴) ∈ ℕ ∧ 1 < 𝑃) → 1 < (𝑃↑(𝑃 pCnt 𝐴))) |
105 | 95, 99, 103, 104 | syl3anc 1491 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 < (𝑃↑(𝑃 pCnt 𝐴))) |
106 | | 1red 10329 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℝ) |
107 | | 0lt1 10842 |
. . . . . . . . . . . . 13
⊢ 0 <
1 |
108 | 107 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < 1) |
109 | 60 | nnred 11329 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℝ) |
110 | 60 | nngt0d 11362 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < (𝑃↑(𝑃 pCnt 𝐴))) |
111 | 16 | nnred 11329 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℝ) |
112 | 16 | nngt0d 11362 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < 𝐴) |
113 | | ltdiv2 11201 |
. . . . . . . . . . . 12
⊢ (((1
∈ ℝ ∧ 0 < 1) ∧ ((𝑃↑(𝑃 pCnt 𝐴)) ∈ ℝ ∧ 0 < (𝑃↑(𝑃 pCnt 𝐴))) ∧ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) → (1 < (𝑃↑(𝑃 pCnt 𝐴)) ↔ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) < (𝐴 / 1))) |
114 | 106, 108,
109, 110, 111, 112, 113 | syl222anc 1506 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 < (𝑃↑(𝑃 pCnt 𝐴)) ↔ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) < (𝐴 / 1))) |
115 | 105, 114 | mpbid 224 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) < (𝐴 / 1)) |
116 | 17 | div1d 11085 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 / 1) = 𝐴) |
117 | 115, 116 | breqtrd 4869 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) < 𝐴) |
118 | | elfzo2 12728 |
. . . . . . . . 9
⊢ ((𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ (1..^𝐴) ↔ ((𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ (ℤ≥‘1)
∧ 𝐴 ∈ ℤ
∧ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) < 𝐴)) |
119 | 93, 94, 117, 118 | syl3anbrc 1444 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ (1..^𝐴)) |
120 | 90, 91, 119 | rspcdva 3503 |
. . . . . . 7
⊢ (𝜑 → if((√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) ≤ (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) |
121 | 120 | adantr 473 |
. . . . . 6
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
if((√‘(𝐴 /
(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) ≤ (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) |
122 | 85, 121 | eqbrtrrd 4867 |
. . . . 5
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 1 ≤
(𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) |
123 | | 1re 10328 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
124 | | 0le1 10843 |
. . . . . . . 8
⊢ 0 ≤
1 |
125 | 123, 124 | pm3.2i 463 |
. . . . . . 7
⊢ (1 ∈
ℝ ∧ 0 ≤ 1) |
126 | 125 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (1
∈ ℝ ∧ 0 ≤ 1)) |
127 | 44, 45, 46, 47, 48, 49, 50, 51, 52 | dchrisum0ff 25548 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:ℕ⟶ℝ) |
128 | 127, 60 | ffvelrnd 6586 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℝ) |
129 | 128 | adantr 473 |
. . . . . 6
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℝ) |
130 | 127, 63 | ffvelrnd 6586 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℝ) |
131 | 130 | adantr 473 |
. . . . . 6
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℝ) |
132 | | lemul12a 11173 |
. . . . . 6
⊢ ((((1
∈ ℝ ∧ 0 ≤ 1) ∧ (𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℝ) ∧ ((1 ∈ ℝ
∧ 0 ≤ 1) ∧ (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℝ)) → ((1 ≤ (𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) ∧ 1 ≤ (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) → (1 · 1) ≤ ((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))))) |
133 | 126, 129,
126, 131, 132 | syl22anc 868 |
. . . . 5
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → ((1
≤ (𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) ∧ 1 ≤ (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) → (1 · 1) ≤ ((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))))) |
134 | 56, 122, 133 | mp2and 691 |
. . . 4
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (1
· 1) ≤ ((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
135 | 3, 134 | syl5eqbrr 4879 |
. . 3
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 1 ≤
((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
136 | | 0red 10332 |
. . . . . 6
⊢ (𝜑 → 0 ∈
ℝ) |
137 | | 0re 10330 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
138 | 123, 137 | ifcli 4323 |
. . . . . . 7
⊢
if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0) ∈
ℝ |
139 | 138 | a1i 11 |
. . . . . 6
⊢ (𝜑 → if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0) ∈
ℝ) |
140 | | breq2 4847 |
. . . . . . . 8
⊢ (1 =
if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0) → (0 ≤ 1
↔ 0 ≤ if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0))) |
141 | | breq2 4847 |
. . . . . . . 8
⊢ (0 =
if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0) → (0 ≤ 0
↔ 0 ≤ if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0))) |
142 | | 0le0 11421 |
. . . . . . . 8
⊢ 0 ≤
0 |
143 | 140, 141,
124, 142 | keephyp 4346 |
. . . . . . 7
⊢ 0 ≤
if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0) |
144 | 143 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 0 ≤
if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0)) |
145 | 136, 139,
128, 144, 54 | letrd 10484 |
. . . . 5
⊢ (𝜑 → 0 ≤ (𝐹‘(𝑃↑(𝑃 pCnt 𝐴)))) |
146 | 123, 137 | ifcli 4323 |
. . . . . . 7
⊢
if((√‘(𝐴
/ (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) ∈
ℝ |
147 | 146 | a1i 11 |
. . . . . 6
⊢ (𝜑 → if((√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) ∈
ℝ) |
148 | | breq2 4847 |
. . . . . . . 8
⊢ (1 =
if((√‘(𝐴 /
(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) → (0 ≤ 1
↔ 0 ≤ if((√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1,
0))) |
149 | | breq2 4847 |
. . . . . . . 8
⊢ (0 =
if((√‘(𝐴 /
(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) → (0 ≤ 0
↔ 0 ≤ if((√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1,
0))) |
150 | 148, 149,
124, 142 | keephyp 4346 |
. . . . . . 7
⊢ 0 ≤
if((√‘(𝐴 /
(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) |
151 | 150 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 0 ≤
if((√‘(𝐴 /
(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0)) |
152 | 136, 147,
130, 151, 120 | letrd 10484 |
. . . . 5
⊢ (𝜑 → 0 ≤ (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) |
153 | 128, 130,
145, 152 | mulge0d 10896 |
. . . 4
⊢ (𝜑 → 0 ≤ ((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
154 | 153 | adantr 473 |
. . 3
⊢ ((𝜑 ∧ ¬ (√‘𝐴) ∈ ℕ) → 0 ≤
((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
155 | 1, 2, 135, 154 | ifbothda 4314 |
. 2
⊢ (𝜑 → if((√‘𝐴) ∈ ℕ, 1, 0) ≤
((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
156 | 60 | nncnd 11330 |
. . . . 5
⊢ (𝜑 → (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℂ) |
157 | 60 | nnne0d 11363 |
. . . . 5
⊢ (𝜑 → (𝑃↑(𝑃 pCnt 𝐴)) ≠ 0) |
158 | 17, 156, 157 | divcan2d 11095 |
. . . 4
⊢ (𝜑 → ((𝑃↑(𝑃 pCnt 𝐴)) · (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 𝐴) |
159 | 158 | fveq2d 6415 |
. . 3
⊢ (𝜑 → (𝐹‘((𝑃↑(𝑃 pCnt 𝐴)) · (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) = (𝐹‘𝐴)) |
160 | | pcndvds2 15905 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) → ¬
𝑃 ∥ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) |
161 | 4, 16, 160 | syl2anc 580 |
. . . . . 6
⊢ (𝜑 → ¬ 𝑃 ∥ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) |
162 | | coprm 15756 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ ℤ) → (¬ 𝑃 ∥ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ↔ (𝑃 gcd (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 1)) |
163 | 4, 64, 162 | syl2anc 580 |
. . . . . 6
⊢ (𝜑 → (¬ 𝑃 ∥ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ↔ (𝑃 gcd (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 1)) |
164 | 161, 163 | mpbid 224 |
. . . . 5
⊢ (𝜑 → (𝑃 gcd (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 1) |
165 | | prmz 15723 |
. . . . . . 7
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
166 | 4, 165 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈ ℤ) |
167 | | rpexp1i 15766 |
. . . . . 6
⊢ ((𝑃 ∈ ℤ ∧ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ ℤ ∧ (𝑃 pCnt 𝐴) ∈ ℕ0) → ((𝑃 gcd (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 1 → ((𝑃↑(𝑃 pCnt 𝐴)) gcd (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 1)) |
168 | 166, 64, 53, 167 | syl3anc 1491 |
. . . . 5
⊢ (𝜑 → ((𝑃 gcd (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 1 → ((𝑃↑(𝑃 pCnt 𝐴)) gcd (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 1)) |
169 | 164, 168 | mpd 15 |
. . . 4
⊢ (𝜑 → ((𝑃↑(𝑃 pCnt 𝐴)) gcd (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 1) |
170 | 44, 45, 46, 47, 48, 49, 50, 51, 60, 63, 169 | dchrisum0fmul 25547 |
. . 3
⊢ (𝜑 → (𝐹‘((𝑃↑(𝑃 pCnt 𝐴)) · (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) = ((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
171 | 159, 170 | eqtr3d 2835 |
. 2
⊢ (𝜑 → (𝐹‘𝐴) = ((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
172 | 155, 171 | breqtrrd 4871 |
1
⊢ (𝜑 → if((√‘𝐴) ∈ ℕ, 1, 0) ≤
(𝐹‘𝐴)) |