Proof of Theorem dchrisum0flblem2
Step | Hyp | Ref
| Expression |
1 | | breq1 4586 |
. . 3
⊢ (1 =
if((√‘𝐴) ∈
ℕ, 1, 0) → (1 ≤ ((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) ↔ if((√‘𝐴) ∈ ℕ, 1, 0) ≤
((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))))) |
2 | | breq1 4586 |
. . 3
⊢ (0 =
if((√‘𝐴) ∈
ℕ, 1, 0) → (0 ≤ ((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) ↔ if((√‘𝐴) ∈ ℕ, 1, 0) ≤
((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))))) |
3 | | 1t1e1 11052 |
. . . 4
⊢ (1
· 1) = 1 |
4 | | dchrisum0flb.2 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑃 ∈ ℙ) |
5 | 4 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 𝑃 ∈
ℙ) |
6 | | nnq 11677 |
. . . . . . . . . . . . . . 15
⊢
((√‘𝐴)
∈ ℕ → (√‘𝐴) ∈ ℚ) |
7 | 6 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘𝐴) ∈
ℚ) |
8 | | nnne0 10930 |
. . . . . . . . . . . . . . 15
⊢
((√‘𝐴)
∈ ℕ → (√‘𝐴) ≠ 0) |
9 | 8 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘𝐴) ≠
0) |
10 | | 2z 11286 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℤ |
11 | 10 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 2
∈ ℤ) |
12 | | pcexp 15402 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧
((√‘𝐴) ∈
ℚ ∧ (√‘𝐴) ≠ 0) ∧ 2 ∈ ℤ) →
(𝑃 pCnt
((√‘𝐴)↑2))
= (2 · (𝑃 pCnt
(√‘𝐴)))) |
13 | 5, 7, 9, 11, 12 | syl121anc 1323 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃 pCnt ((√‘𝐴)↑2)) = (2 · (𝑃 pCnt (√‘𝐴)))) |
14 | | dchrisum0flb.1 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ∈
(ℤ≥‘2)) |
15 | | eluz2nn 11602 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈
(ℤ≥‘2) → 𝐴 ∈ ℕ) |
16 | 14, 15 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐴 ∈ ℕ) |
17 | 16 | nncnd 10913 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ∈ ℂ) |
18 | 17 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 𝐴 ∈
ℂ) |
19 | 18 | sqsqrtd 14026 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
((√‘𝐴)↑2)
= 𝐴) |
20 | 19 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃 pCnt ((√‘𝐴)↑2)) = (𝑃 pCnt 𝐴)) |
21 | | 2cnd 10970 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 2
∈ ℂ) |
22 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘𝐴) ∈
ℕ) |
23 | 5, 22 | pccld 15393 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃 pCnt (√‘𝐴)) ∈
ℕ0) |
24 | 23 | nn0cnd 11230 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃 pCnt (√‘𝐴)) ∈
ℂ) |
25 | 21, 24 | mulcomd 9940 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (2
· (𝑃 pCnt
(√‘𝐴))) =
((𝑃 pCnt
(√‘𝐴)) ·
2)) |
26 | 13, 20, 25 | 3eqtr3rd 2653 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → ((𝑃 pCnt (√‘𝐴)) · 2) = (𝑃 pCnt 𝐴)) |
27 | 26 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃↑((𝑃 pCnt (√‘𝐴)) · 2)) = (𝑃↑(𝑃 pCnt 𝐴))) |
28 | | prmnn 15226 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
29 | 5, 28 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 𝑃 ∈
ℕ) |
30 | 29 | nncnd 10913 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 𝑃 ∈
ℂ) |
31 | | 2nn0 11186 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℕ0 |
32 | 31 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 2
∈ ℕ0) |
33 | 30, 32, 23 | expmuld 12873 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃↑((𝑃 pCnt (√‘𝐴)) · 2)) = ((𝑃↑(𝑃 pCnt (√‘𝐴)))↑2)) |
34 | 27, 33 | eqtr3d 2646 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃↑(𝑃 pCnt 𝐴)) = ((𝑃↑(𝑃 pCnt (√‘𝐴)))↑2)) |
35 | 34 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘(𝑃↑(𝑃 pCnt 𝐴))) = (√‘((𝑃↑(𝑃 pCnt (√‘𝐴)))↑2))) |
36 | 29, 23 | nnexpcld 12892 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃↑(𝑃 pCnt (√‘𝐴))) ∈ ℕ) |
37 | 36 | nnrpd 11746 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃↑(𝑃 pCnt (√‘𝐴))) ∈
ℝ+) |
38 | 37 | rprege0d 11755 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → ((𝑃↑(𝑃 pCnt (√‘𝐴))) ∈ ℝ ∧ 0 ≤ (𝑃↑(𝑃 pCnt (√‘𝐴))))) |
39 | | sqrtsq 13858 |
. . . . . . . . . 10
⊢ (((𝑃↑(𝑃 pCnt (√‘𝐴))) ∈ ℝ ∧ 0 ≤ (𝑃↑(𝑃 pCnt (√‘𝐴)))) → (√‘((𝑃↑(𝑃 pCnt (√‘𝐴)))↑2)) = (𝑃↑(𝑃 pCnt (√‘𝐴)))) |
40 | 38, 39 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘((𝑃↑(𝑃 pCnt (√‘𝐴)))↑2)) = (𝑃↑(𝑃 pCnt (√‘𝐴)))) |
41 | 35, 40 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘(𝑃↑(𝑃 pCnt 𝐴))) = (𝑃↑(𝑃 pCnt (√‘𝐴)))) |
42 | 41, 36 | eqeltrd 2688 |
. . . . . . 7
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ) |
43 | 42 | iftrued 4044 |
. . . . . 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 15393 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 pCnt 𝐴) ∈
ℕ0) |
54 | 44, 45, 46, 47, 48, 49, 50, 51, 52, 4, 53 | dchrisum0flblem1 24997 |
. . . . . . 7
⊢ (𝜑 → if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0) ≤ (𝐹‘(𝑃↑(𝑃 pCnt 𝐴)))) |
55 | 54 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0) ≤ (𝐹‘(𝑃↑(𝑃 pCnt 𝐴)))) |
56 | 43, 55 | eqbrtrrd 4607 |
. . . . 5
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 1 ≤
(𝐹‘(𝑃↑(𝑃 pCnt 𝐴)))) |
57 | | pcdvds 15406 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐴) |
58 | 4, 16, 57 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐴) |
59 | 4, 28 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑃 ∈ ℕ) |
60 | 59, 53 | nnexpcld 12892 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℕ) |
61 | | nndivdvds 14827 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ ∧ (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℕ) → ((𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐴 ↔ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ)) |
62 | 16, 60, 61 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐴 ↔ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ)) |
63 | 58, 62 | mpbid 221 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ) |
64 | 63 | nnzd 11357 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ ℤ) |
65 | 64 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ ℤ) |
66 | 16 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 𝐴 ∈
ℕ) |
67 | 66 | nnrpd 11746 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 𝐴 ∈
ℝ+) |
68 | 67 | rprege0d 11755 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝐴 ∈ ℝ ∧ 0 ≤
𝐴)) |
69 | 60 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℕ) |
70 | 69 | nnrpd 11746 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃↑(𝑃 pCnt 𝐴)) ∈
ℝ+) |
71 | | sqrtdiv 13854 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℝ+) →
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = ((√‘𝐴) / (√‘(𝑃↑(𝑃 pCnt 𝐴))))) |
72 | 68, 70, 71 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = ((√‘𝐴) / (√‘(𝑃↑(𝑃 pCnt 𝐴))))) |
73 | | nnz 11276 |
. . . . . . . . . . . 12
⊢
((√‘𝐴)
∈ ℕ → (√‘𝐴) ∈ ℤ) |
74 | 73 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘𝐴) ∈
ℤ) |
75 | | znq 11668 |
. . . . . . . . . . 11
⊢
(((√‘𝐴)
∈ ℤ ∧ (√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ) →
((√‘𝐴) /
(√‘(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℚ) |
76 | 74, 42, 75 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
((√‘𝐴) /
(√‘(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℚ) |
77 | 72, 76 | eqeltrd 2688 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℚ) |
78 | | zsqrtelqelz 15304 |
. . . . . . . . 9
⊢ (((𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ ℤ ∧
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℚ) →
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℤ) |
79 | 65, 77, 78 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℤ) |
80 | 63 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ) |
81 | 80 | nnrpd 11746 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈
ℝ+) |
82 | 81 | sqrtgt0d 13999 |
. . . . . . . 8
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 0 <
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) |
83 | | elnnz 11264 |
. . . . . . . 8
⊢
((√‘(𝐴 /
(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ ↔
((√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℤ ∧ 0 <
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
84 | 79, 82, 83 | sylanbrc 695 |
. . . . . . 7
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ) |
85 | 84 | iftrued 4044 |
. . . . . 6
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
if((√‘(𝐴 /
(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) =
1) |
86 | | nnuz 11599 |
. . . . . . . . . 10
⊢ ℕ =
(ℤ≥‘1) |
87 | 63, 86 | syl6eleq 2698 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈
(ℤ≥‘1)) |
88 | 16 | nnzd 11357 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℤ) |
89 | 59 | nnred 10912 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈ ℝ) |
90 | | dchrisum0flb.3 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 ∥ 𝐴) |
91 | | pcelnn 15412 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) → ((𝑃 pCnt 𝐴) ∈ ℕ ↔ 𝑃 ∥ 𝐴)) |
92 | 4, 16, 91 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑃 pCnt 𝐴) ∈ ℕ ↔ 𝑃 ∥ 𝐴)) |
93 | 90, 92 | mpbird 246 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑃 pCnt 𝐴) ∈ ℕ) |
94 | | prmuz2 15246 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
95 | | eluz2b2 11637 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈
(ℤ≥‘2) ↔ (𝑃 ∈ ℕ ∧ 1 < 𝑃)) |
96 | 95 | simprbi 479 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈
(ℤ≥‘2) → 1 < 𝑃) |
97 | 4, 94, 96 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 < 𝑃) |
98 | | expgt1 12760 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℝ ∧ (𝑃 pCnt 𝐴) ∈ ℕ ∧ 1 < 𝑃) → 1 < (𝑃↑(𝑃 pCnt 𝐴))) |
99 | 89, 93, 97, 98 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 < (𝑃↑(𝑃 pCnt 𝐴))) |
100 | | 1red 9934 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℝ) |
101 | | 0lt1 10429 |
. . . . . . . . . . . . 13
⊢ 0 <
1 |
102 | 101 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < 1) |
103 | 60 | nnred 10912 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℝ) |
104 | 60 | nngt0d 10941 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < (𝑃↑(𝑃 pCnt 𝐴))) |
105 | 16 | nnred 10912 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℝ) |
106 | 16 | nngt0d 10941 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < 𝐴) |
107 | | ltdiv2 10788 |
. . . . . . . . . . . 12
⊢ (((1
∈ ℝ ∧ 0 < 1) ∧ ((𝑃↑(𝑃 pCnt 𝐴)) ∈ ℝ ∧ 0 < (𝑃↑(𝑃 pCnt 𝐴))) ∧ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) → (1 < (𝑃↑(𝑃 pCnt 𝐴)) ↔ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) < (𝐴 / 1))) |
108 | 100, 102,
103, 104, 105, 106, 107 | syl222anc 1334 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 < (𝑃↑(𝑃 pCnt 𝐴)) ↔ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) < (𝐴 / 1))) |
109 | 99, 108 | mpbid 221 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) < (𝐴 / 1)) |
110 | 17 | div1d 10672 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 / 1) = 𝐴) |
111 | 109, 110 | breqtrd 4609 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) < 𝐴) |
112 | | elfzo2 12342 |
. . . . . . . . 9
⊢ ((𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ (1..^𝐴) ↔ ((𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ (ℤ≥‘1)
∧ 𝐴 ∈ ℤ
∧ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) < 𝐴)) |
113 | 87, 88, 111, 112 | syl3anbrc 1239 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ (1..^𝐴)) |
114 | | dchrisum0flb.4 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑦 ∈ (1..^𝐴)if((√‘𝑦) ∈ ℕ, 1, 0) ≤ (𝐹‘𝑦)) |
115 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) → (√‘𝑦) = (√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) |
116 | 115 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) → ((√‘𝑦) ∈ ℕ ↔
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ)) |
117 | 116 | ifbid 4058 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) → if((√‘𝑦) ∈ ℕ, 1, 0) =
if((√‘(𝐴 /
(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0)) |
118 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) → (𝐹‘𝑦) = (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) |
119 | 117, 118 | breq12d 4596 |
. . . . . . . . 9
⊢ (𝑦 = (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) → (if((√‘𝑦) ∈ ℕ, 1, 0) ≤
(𝐹‘𝑦) ↔ if((√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) ≤ (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
120 | 119 | rspcv 3278 |
. . . . . . . 8
⊢ ((𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ (1..^𝐴) → (∀𝑦 ∈ (1..^𝐴)if((√‘𝑦) ∈ ℕ, 1, 0) ≤ (𝐹‘𝑦) → if((√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) ≤ (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
121 | 113, 114,
120 | sylc 63 |
. . . . . . 7
⊢ (𝜑 → if((√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) ≤ (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) |
122 | 121 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
if((√‘(𝐴 /
(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) ≤ (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) |
123 | 85, 122 | eqbrtrrd 4607 |
. . . . 5
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 1 ≤
(𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) |
124 | | 1re 9918 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
125 | | 0le1 10430 |
. . . . . . . 8
⊢ 0 ≤
1 |
126 | 124, 125 | pm3.2i 470 |
. . . . . . 7
⊢ (1 ∈
ℝ ∧ 0 ≤ 1) |
127 | 126 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (1
∈ ℝ ∧ 0 ≤ 1)) |
128 | 44, 45, 46, 47, 48, 49, 50, 51, 52 | dchrisum0ff 24996 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:ℕ⟶ℝ) |
129 | 128, 60 | ffvelrnd 6268 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℝ) |
130 | 129 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℝ) |
131 | 128, 63 | ffvelrnd 6268 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℝ) |
132 | 131 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℝ) |
133 | | lemul12a 10760 |
. . . . . 6
⊢ ((((1
∈ ℝ ∧ 0 ≤ 1) ∧ (𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℝ) ∧ ((1 ∈ ℝ
∧ 0 ≤ 1) ∧ (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℝ)) → ((1 ≤ (𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) ∧ 1 ≤ (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) → (1 · 1) ≤ ((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))))) |
134 | 127, 130,
127, 132, 133 | syl22anc 1319 |
. . . . 5
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → ((1
≤ (𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) ∧ 1 ≤ (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) → (1 · 1) ≤ ((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))))) |
135 | 56, 123, 134 | mp2and 711 |
. . . 4
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (1
· 1) ≤ ((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
136 | 3, 135 | syl5eqbrr 4619 |
. . 3
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 1 ≤
((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
137 | | 0red 9920 |
. . . . . 6
⊢ (𝜑 → 0 ∈
ℝ) |
138 | | 0re 9919 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
139 | 124, 138 | keepel 4105 |
. . . . . . 7
⊢
if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0) ∈
ℝ |
140 | 139 | a1i 11 |
. . . . . 6
⊢ (𝜑 → if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0) ∈
ℝ) |
141 | | breq2 4587 |
. . . . . . . 8
⊢ (1 =
if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0) → (0 ≤ 1
↔ 0 ≤ if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0))) |
142 | | breq2 4587 |
. . . . . . . 8
⊢ (0 =
if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0) → (0 ≤ 0
↔ 0 ≤ if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0))) |
143 | | 0le0 10987 |
. . . . . . . 8
⊢ 0 ≤
0 |
144 | 141, 142,
125, 143 | keephyp 4102 |
. . . . . . 7
⊢ 0 ≤
if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0) |
145 | 144 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 0 ≤
if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0)) |
146 | 137, 140,
129, 145, 54 | letrd 10073 |
. . . . 5
⊢ (𝜑 → 0 ≤ (𝐹‘(𝑃↑(𝑃 pCnt 𝐴)))) |
147 | 124, 138 | keepel 4105 |
. . . . . . 7
⊢
if((√‘(𝐴
/ (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) ∈
ℝ |
148 | 147 | a1i 11 |
. . . . . 6
⊢ (𝜑 → if((√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) ∈
ℝ) |
149 | | breq2 4587 |
. . . . . . . 8
⊢ (1 =
if((√‘(𝐴 /
(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) → (0 ≤ 1
↔ 0 ≤ if((√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1,
0))) |
150 | | breq2 4587 |
. . . . . . . 8
⊢ (0 =
if((√‘(𝐴 /
(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) → (0 ≤ 0
↔ 0 ≤ if((√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1,
0))) |
151 | 149, 150,
125, 143 | keephyp 4102 |
. . . . . . 7
⊢ 0 ≤
if((√‘(𝐴 /
(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) |
152 | 151 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 0 ≤
if((√‘(𝐴 /
(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0)) |
153 | 137, 148,
131, 152, 121 | letrd 10073 |
. . . . 5
⊢ (𝜑 → 0 ≤ (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) |
154 | 129, 131,
146, 153 | mulge0d 10483 |
. . . 4
⊢ (𝜑 → 0 ≤ ((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
155 | 154 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ ¬ (√‘𝐴) ∈ ℕ) → 0 ≤
((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
156 | 1, 2, 136, 155 | ifbothda 4073 |
. 2
⊢ (𝜑 → if((√‘𝐴) ∈ ℕ, 1, 0) ≤
((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
157 | 60 | nncnd 10913 |
. . . . 5
⊢ (𝜑 → (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℂ) |
158 | 60 | nnne0d 10942 |
. . . . 5
⊢ (𝜑 → (𝑃↑(𝑃 pCnt 𝐴)) ≠ 0) |
159 | 17, 157, 158 | divcan2d 10682 |
. . . 4
⊢ (𝜑 → ((𝑃↑(𝑃 pCnt 𝐴)) · (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 𝐴) |
160 | 159 | fveq2d 6107 |
. . 3
⊢ (𝜑 → (𝐹‘((𝑃↑(𝑃 pCnt 𝐴)) · (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) = (𝐹‘𝐴)) |
161 | | pcndvds2 15410 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) → ¬
𝑃 ∥ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) |
162 | 4, 16, 161 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → ¬ 𝑃 ∥ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) |
163 | | coprm 15261 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ ℤ) → (¬ 𝑃 ∥ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ↔ (𝑃 gcd (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 1)) |
164 | 4, 64, 163 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (¬ 𝑃 ∥ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ↔ (𝑃 gcd (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 1)) |
165 | 162, 164 | mpbid 221 |
. . . . 5
⊢ (𝜑 → (𝑃 gcd (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 1) |
166 | | prmz 15227 |
. . . . . . 7
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
167 | 4, 166 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈ ℤ) |
168 | | rpexp1i 15271 |
. . . . . 6
⊢ ((𝑃 ∈ ℤ ∧ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ ℤ ∧ (𝑃 pCnt 𝐴) ∈ ℕ0) → ((𝑃 gcd (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 1 → ((𝑃↑(𝑃 pCnt 𝐴)) gcd (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 1)) |
169 | 167, 64, 53, 168 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → ((𝑃 gcd (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 1 → ((𝑃↑(𝑃 pCnt 𝐴)) gcd (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 1)) |
170 | 165, 169 | mpd 15 |
. . . 4
⊢ (𝜑 → ((𝑃↑(𝑃 pCnt 𝐴)) gcd (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 1) |
171 | 44, 45, 46, 47, 48, 49, 50, 51, 60, 63, 170 | dchrisum0fmul 24995 |
. . 3
⊢ (𝜑 → (𝐹‘((𝑃↑(𝑃 pCnt 𝐴)) · (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) = ((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
172 | 160, 171 | eqtr3d 2646 |
. 2
⊢ (𝜑 → (𝐹‘𝐴) = ((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
173 | 156, 172 | breqtrrd 4611 |
1
⊢ (𝜑 → if((√‘𝐴) ∈ ℕ, 1, 0) ≤
(𝐹‘𝐴)) |