Proof of Theorem dchrisum0flblem2
Step | Hyp | Ref
| Expression |
1 | | breq1 4656 |
. . 3
⊢ (1 =
if((√‘𝐴) ∈
ℕ, 1, 0) → (1 ≤ ((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) ↔ if((√‘𝐴) ∈ ℕ, 1, 0) ≤
((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))))) |
2 | | breq1 4656 |
. . 3
⊢ (0 =
if((√‘𝐴) ∈
ℕ, 1, 0) → (0 ≤ ((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) ↔ if((√‘𝐴) ∈ ℕ, 1, 0) ≤
((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))))) |
3 | | 1t1e1 11175 |
. . . 4
⊢ (1
· 1) = 1 |
4 | | dchrisum0flb.2 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑃 ∈ ℙ) |
5 | 4 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 𝑃 ∈
ℙ) |
6 | | nnq 11801 |
. . . . . . . . . . . . . . 15
⊢
((√‘𝐴)
∈ ℕ → (√‘𝐴) ∈ ℚ) |
7 | 6 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘𝐴) ∈
ℚ) |
8 | | nnne0 11053 |
. . . . . . . . . . . . . . 15
⊢
((√‘𝐴)
∈ ℕ → (√‘𝐴) ≠ 0) |
9 | 8 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘𝐴) ≠
0) |
10 | | 2z 11409 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℤ |
11 | 10 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 2
∈ ℤ) |
12 | | pcexp 15564 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧
((√‘𝐴) ∈
ℚ ∧ (√‘𝐴) ≠ 0) ∧ 2 ∈ ℤ) →
(𝑃 pCnt
((√‘𝐴)↑2))
= (2 · (𝑃 pCnt
(√‘𝐴)))) |
13 | 5, 7, 9, 11, 12 | syl121anc 1331 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃 pCnt ((√‘𝐴)↑2)) = (2 · (𝑃 pCnt (√‘𝐴)))) |
14 | | dchrisum0flb.1 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ∈
(ℤ≥‘2)) |
15 | | eluz2nn 11726 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈
(ℤ≥‘2) → 𝐴 ∈ ℕ) |
16 | 14, 15 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐴 ∈ ℕ) |
17 | 16 | nncnd 11036 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ∈ ℂ) |
18 | 17 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 𝐴 ∈
ℂ) |
19 | 18 | sqsqrtd 14178 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
((√‘𝐴)↑2)
= 𝐴) |
20 | 19 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃 pCnt ((√‘𝐴)↑2)) = (𝑃 pCnt 𝐴)) |
21 | | 2cnd 11093 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 2
∈ ℂ) |
22 | | simpr 477 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘𝐴) ∈
ℕ) |
23 | 5, 22 | pccld 15555 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃 pCnt (√‘𝐴)) ∈
ℕ0) |
24 | 23 | nn0cnd 11353 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃 pCnt (√‘𝐴)) ∈
ℂ) |
25 | 21, 24 | mulcomd 10061 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (2
· (𝑃 pCnt
(√‘𝐴))) =
((𝑃 pCnt
(√‘𝐴)) ·
2)) |
26 | 13, 20, 25 | 3eqtr3rd 2665 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → ((𝑃 pCnt (√‘𝐴)) · 2) = (𝑃 pCnt 𝐴)) |
27 | 26 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃↑((𝑃 pCnt (√‘𝐴)) · 2)) = (𝑃↑(𝑃 pCnt 𝐴))) |
28 | | prmnn 15388 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
29 | 5, 28 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 𝑃 ∈
ℕ) |
30 | 29 | nncnd 11036 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 𝑃 ∈
ℂ) |
31 | | 2nn0 11309 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℕ0 |
32 | 31 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 2
∈ ℕ0) |
33 | 30, 32, 23 | expmuld 13011 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃↑((𝑃 pCnt (√‘𝐴)) · 2)) = ((𝑃↑(𝑃 pCnt (√‘𝐴)))↑2)) |
34 | 27, 33 | eqtr3d 2658 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃↑(𝑃 pCnt 𝐴)) = ((𝑃↑(𝑃 pCnt (√‘𝐴)))↑2)) |
35 | 34 | fveq2d 6195 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘(𝑃↑(𝑃 pCnt 𝐴))) = (√‘((𝑃↑(𝑃 pCnt (√‘𝐴)))↑2))) |
36 | 29, 23 | nnexpcld 13030 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃↑(𝑃 pCnt (√‘𝐴))) ∈ ℕ) |
37 | 36 | nnrpd 11870 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃↑(𝑃 pCnt (√‘𝐴))) ∈
ℝ+) |
38 | 37 | rprege0d 11879 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → ((𝑃↑(𝑃 pCnt (√‘𝐴))) ∈ ℝ ∧ 0 ≤ (𝑃↑(𝑃 pCnt (√‘𝐴))))) |
39 | | sqrtsq 14010 |
. . . . . . . . . 10
⊢ (((𝑃↑(𝑃 pCnt (√‘𝐴))) ∈ ℝ ∧ 0 ≤ (𝑃↑(𝑃 pCnt (√‘𝐴)))) → (√‘((𝑃↑(𝑃 pCnt (√‘𝐴)))↑2)) = (𝑃↑(𝑃 pCnt (√‘𝐴)))) |
40 | 38, 39 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘((𝑃↑(𝑃 pCnt (√‘𝐴)))↑2)) = (𝑃↑(𝑃 pCnt (√‘𝐴)))) |
41 | 35, 40 | eqtrd 2656 |
. . . . . . . 8
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘(𝑃↑(𝑃 pCnt 𝐴))) = (𝑃↑(𝑃 pCnt (√‘𝐴)))) |
42 | 41, 36 | eqeltrd 2701 |
. . . . . . 7
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ) |
43 | 42 | iftrued 4094 |
. . . . . 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 15555 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 pCnt 𝐴) ∈
ℕ0) |
54 | 44, 45, 46, 47, 48, 49, 50, 51, 52, 4, 53 | dchrisum0flblem1 25197 |
. . . . . . 7
⊢ (𝜑 → if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0) ≤ (𝐹‘(𝑃↑(𝑃 pCnt 𝐴)))) |
55 | 54 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0) ≤ (𝐹‘(𝑃↑(𝑃 pCnt 𝐴)))) |
56 | 43, 55 | eqbrtrrd 4677 |
. . . . 5
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 1 ≤
(𝐹‘(𝑃↑(𝑃 pCnt 𝐴)))) |
57 | | pcdvds 15568 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐴) |
58 | 4, 16, 57 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐴) |
59 | 4, 28 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑃 ∈ ℕ) |
60 | 59, 53 | nnexpcld 13030 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℕ) |
61 | | nndivdvds 14989 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ ∧ (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℕ) → ((𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐴 ↔ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ)) |
62 | 16, 60, 61 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐴 ↔ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ)) |
63 | 58, 62 | mpbid 222 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ) |
64 | 63 | nnzd 11481 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ ℤ) |
65 | 64 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ ℤ) |
66 | 16 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 𝐴 ∈
ℕ) |
67 | 66 | nnrpd 11870 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 𝐴 ∈
ℝ+) |
68 | 67 | rprege0d 11879 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝐴 ∈ ℝ ∧ 0 ≤
𝐴)) |
69 | 60 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℕ) |
70 | 69 | nnrpd 11870 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝑃↑(𝑃 pCnt 𝐴)) ∈
ℝ+) |
71 | | sqrtdiv 14006 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℝ+) →
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = ((√‘𝐴) / (√‘(𝑃↑(𝑃 pCnt 𝐴))))) |
72 | 68, 70, 71 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = ((√‘𝐴) / (√‘(𝑃↑(𝑃 pCnt 𝐴))))) |
73 | | nnz 11399 |
. . . . . . . . . . . 12
⊢
((√‘𝐴)
∈ ℕ → (√‘𝐴) ∈ ℤ) |
74 | 73 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘𝐴) ∈
ℤ) |
75 | | znq 11792 |
. . . . . . . . . . 11
⊢
(((√‘𝐴)
∈ ℤ ∧ (√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ) →
((√‘𝐴) /
(√‘(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℚ) |
76 | 74, 42, 75 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
((√‘𝐴) /
(√‘(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℚ) |
77 | 72, 76 | eqeltrd 2701 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℚ) |
78 | | zsqrtelqelz 15466 |
. . . . . . . . 9
⊢ (((𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ ℤ ∧
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℚ) →
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℤ) |
79 | 65, 77, 78 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℤ) |
80 | 63 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ) |
81 | 80 | nnrpd 11870 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈
ℝ+) |
82 | 81 | sqrtgt0d 14151 |
. . . . . . . 8
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 0 <
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) |
83 | | elnnz 11387 |
. . . . . . . 8
⊢
((√‘(𝐴 /
(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ ↔
((√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℤ ∧ 0 <
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
84 | 79, 82, 83 | sylanbrc 698 |
. . . . . . 7
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ) |
85 | 84 | iftrued 4094 |
. . . . . 6
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
if((√‘(𝐴 /
(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) =
1) |
86 | | nnuz 11723 |
. . . . . . . . . 10
⊢ ℕ =
(ℤ≥‘1) |
87 | 63, 86 | syl6eleq 2711 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈
(ℤ≥‘1)) |
88 | 16 | nnzd 11481 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℤ) |
89 | 59 | nnred 11035 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈ ℝ) |
90 | | dchrisum0flb.3 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 ∥ 𝐴) |
91 | | pcelnn 15574 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) → ((𝑃 pCnt 𝐴) ∈ ℕ ↔ 𝑃 ∥ 𝐴)) |
92 | 4, 16, 91 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑃 pCnt 𝐴) ∈ ℕ ↔ 𝑃 ∥ 𝐴)) |
93 | 90, 92 | mpbird 247 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑃 pCnt 𝐴) ∈ ℕ) |
94 | | prmuz2 15408 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
95 | | eluz2b2 11761 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈
(ℤ≥‘2) ↔ (𝑃 ∈ ℕ ∧ 1 < 𝑃)) |
96 | 95 | simprbi 480 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈
(ℤ≥‘2) → 1 < 𝑃) |
97 | 4, 94, 96 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 < 𝑃) |
98 | | expgt1 12898 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℝ ∧ (𝑃 pCnt 𝐴) ∈ ℕ ∧ 1 < 𝑃) → 1 < (𝑃↑(𝑃 pCnt 𝐴))) |
99 | 89, 93, 97, 98 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 < (𝑃↑(𝑃 pCnt 𝐴))) |
100 | | 1red 10055 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℝ) |
101 | | 0lt1 10550 |
. . . . . . . . . . . . 13
⊢ 0 <
1 |
102 | 101 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < 1) |
103 | 60 | nnred 11035 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℝ) |
104 | 60 | nngt0d 11064 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < (𝑃↑(𝑃 pCnt 𝐴))) |
105 | 16 | nnred 11035 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℝ) |
106 | 16 | nngt0d 11064 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < 𝐴) |
107 | | ltdiv2 10909 |
. . . . . . . . . . . 12
⊢ (((1
∈ ℝ ∧ 0 < 1) ∧ ((𝑃↑(𝑃 pCnt 𝐴)) ∈ ℝ ∧ 0 < (𝑃↑(𝑃 pCnt 𝐴))) ∧ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) → (1 < (𝑃↑(𝑃 pCnt 𝐴)) ↔ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) < (𝐴 / 1))) |
108 | 100, 102,
103, 104, 105, 106, 107 | syl222anc 1342 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 < (𝑃↑(𝑃 pCnt 𝐴)) ↔ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) < (𝐴 / 1))) |
109 | 99, 108 | mpbid 222 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) < (𝐴 / 1)) |
110 | 17 | div1d 10793 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 / 1) = 𝐴) |
111 | 109, 110 | breqtrd 4679 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) < 𝐴) |
112 | | elfzo2 12473 |
. . . . . . . . 9
⊢ ((𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ (1..^𝐴) ↔ ((𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ (ℤ≥‘1)
∧ 𝐴 ∈ ℤ
∧ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) < 𝐴)) |
113 | 87, 88, 111, 112 | syl3anbrc 1246 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ (1..^𝐴)) |
114 | | dchrisum0flb.4 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑦 ∈ (1..^𝐴)if((√‘𝑦) ∈ ℕ, 1, 0) ≤ (𝐹‘𝑦)) |
115 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) → (√‘𝑦) = (√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) |
116 | 115 | eleq1d 2686 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) → ((√‘𝑦) ∈ ℕ ↔
(√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ)) |
117 | 116 | ifbid 4108 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) → if((√‘𝑦) ∈ ℕ, 1, 0) =
if((√‘(𝐴 /
(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0)) |
118 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) → (𝐹‘𝑦) = (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) |
119 | 117, 118 | breq12d 4666 |
. . . . . . . . 9
⊢ (𝑦 = (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) → (if((√‘𝑦) ∈ ℕ, 1, 0) ≤
(𝐹‘𝑦) ↔ if((√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) ≤ (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
120 | 119 | rspcv 3305 |
. . . . . . . 8
⊢ ((𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ (1..^𝐴) → (∀𝑦 ∈ (1..^𝐴)if((√‘𝑦) ∈ ℕ, 1, 0) ≤ (𝐹‘𝑦) → if((√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) ≤ (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
121 | 113, 114,
120 | sylc 65 |
. . . . . . 7
⊢ (𝜑 → if((√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) ≤ (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) |
122 | 121 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) →
if((√‘(𝐴 /
(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) ≤ (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) |
123 | 85, 122 | eqbrtrrd 4677 |
. . . . 5
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 1 ≤
(𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) |
124 | | 1re 10039 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
125 | | 0le1 10551 |
. . . . . . . 8
⊢ 0 ≤
1 |
126 | 124, 125 | pm3.2i 471 |
. . . . . . 7
⊢ (1 ∈
ℝ ∧ 0 ≤ 1) |
127 | 126 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (1
∈ ℝ ∧ 0 ≤ 1)) |
128 | 44, 45, 46, 47, 48, 49, 50, 51, 52 | dchrisum0ff 25196 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:ℕ⟶ℝ) |
129 | 128, 60 | ffvelrnd 6360 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℝ) |
130 | 129 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℝ) |
131 | 128, 63 | ffvelrnd 6360 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℝ) |
132 | 131 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℝ) |
133 | | lemul12a 10881 |
. . . . . 6
⊢ ((((1
∈ ℝ ∧ 0 ≤ 1) ∧ (𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℝ) ∧ ((1 ∈ ℝ
∧ 0 ≤ 1) ∧ (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℝ)) → ((1 ≤ (𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) ∧ 1 ≤ (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) → (1 · 1) ≤ ((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))))) |
134 | 127, 130,
127, 132, 133 | syl22anc 1327 |
. . . . 5
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → ((1
≤ (𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) ∧ 1 ≤ (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) → (1 · 1) ≤ ((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))))) |
135 | 56, 123, 134 | mp2and 715 |
. . . 4
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → (1
· 1) ≤ ((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
136 | 3, 135 | syl5eqbrr 4689 |
. . 3
⊢ ((𝜑 ∧ (√‘𝐴) ∈ ℕ) → 1 ≤
((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
137 | | 0red 10041 |
. . . . . 6
⊢ (𝜑 → 0 ∈
ℝ) |
138 | | 0re 10040 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
139 | 124, 138 | keepel 4155 |
. . . . . . 7
⊢
if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0) ∈
ℝ |
140 | 139 | a1i 11 |
. . . . . 6
⊢ (𝜑 → if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0) ∈
ℝ) |
141 | | breq2 4657 |
. . . . . . . 8
⊢ (1 =
if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0) → (0 ≤ 1
↔ 0 ≤ if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0))) |
142 | | breq2 4657 |
. . . . . . . 8
⊢ (0 =
if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0) → (0 ≤ 0
↔ 0 ≤ if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0))) |
143 | | 0le0 11110 |
. . . . . . . 8
⊢ 0 ≤
0 |
144 | 141, 142,
125, 143 | keephyp 4152 |
. . . . . . 7
⊢ 0 ≤
if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0) |
145 | 144 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 0 ≤
if((√‘(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℕ, 1, 0)) |
146 | 137, 140,
129, 145, 54 | letrd 10194 |
. . . . 5
⊢ (𝜑 → 0 ≤ (𝐹‘(𝑃↑(𝑃 pCnt 𝐴)))) |
147 | 124, 138 | keepel 4155 |
. . . . . . 7
⊢
if((√‘(𝐴
/ (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) ∈
ℝ |
148 | 147 | a1i 11 |
. . . . . 6
⊢ (𝜑 → if((√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) ∈
ℝ) |
149 | | breq2 4657 |
. . . . . . . 8
⊢ (1 =
if((√‘(𝐴 /
(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) → (0 ≤ 1
↔ 0 ≤ if((√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1,
0))) |
150 | | breq2 4657 |
. . . . . . . 8
⊢ (0 =
if((√‘(𝐴 /
(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) → (0 ≤ 0
↔ 0 ≤ if((√‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1,
0))) |
151 | 149, 150,
125, 143 | keephyp 4152 |
. . . . . . 7
⊢ 0 ≤
if((√‘(𝐴 /
(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0) |
152 | 151 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 0 ≤
if((√‘(𝐴 /
(𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℕ, 1, 0)) |
153 | 137, 148,
131, 152, 121 | letrd 10194 |
. . . . 5
⊢ (𝜑 → 0 ≤ (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) |
154 | 129, 131,
146, 153 | mulge0d 10604 |
. . . 4
⊢ (𝜑 → 0 ≤ ((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
155 | 154 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ ¬ (√‘𝐴) ∈ ℕ) → 0 ≤
((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
156 | 1, 2, 136, 155 | ifbothda 4123 |
. 2
⊢ (𝜑 → if((√‘𝐴) ∈ ℕ, 1, 0) ≤
((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
157 | 60 | nncnd 11036 |
. . . . 5
⊢ (𝜑 → (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℂ) |
158 | 60 | nnne0d 11065 |
. . . . 5
⊢ (𝜑 → (𝑃↑(𝑃 pCnt 𝐴)) ≠ 0) |
159 | 17, 157, 158 | divcan2d 10803 |
. . . 4
⊢ (𝜑 → ((𝑃↑(𝑃 pCnt 𝐴)) · (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 𝐴) |
160 | 159 | fveq2d 6195 |
. . 3
⊢ (𝜑 → (𝐹‘((𝑃↑(𝑃 pCnt 𝐴)) · (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) = (𝐹‘𝐴)) |
161 | | pcndvds2 15572 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) → ¬
𝑃 ∥ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) |
162 | 4, 16, 161 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → ¬ 𝑃 ∥ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) |
163 | | coprm 15423 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ ℤ) → (¬ 𝑃 ∥ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ↔ (𝑃 gcd (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 1)) |
164 | 4, 64, 163 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → (¬ 𝑃 ∥ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ↔ (𝑃 gcd (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 1)) |
165 | 162, 164 | mpbid 222 |
. . . . 5
⊢ (𝜑 → (𝑃 gcd (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 1) |
166 | | prmz 15389 |
. . . . . . 7
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
167 | 4, 166 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈ ℤ) |
168 | | rpexp1i 15433 |
. . . . . 6
⊢ ((𝑃 ∈ ℤ ∧ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ ℤ ∧ (𝑃 pCnt 𝐴) ∈ ℕ0) → ((𝑃 gcd (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 1 → ((𝑃↑(𝑃 pCnt 𝐴)) gcd (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 1)) |
169 | 167, 64, 53, 168 | syl3anc 1326 |
. . . . 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 25195 |
. . 3
⊢ (𝜑 → (𝐹‘((𝑃↑(𝑃 pCnt 𝐴)) · (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) = ((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
172 | 160, 171 | eqtr3d 2658 |
. 2
⊢ (𝜑 → (𝐹‘𝐴) = ((𝐹‘(𝑃↑(𝑃 pCnt 𝐴))) · (𝐹‘(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))) |
173 | 156, 172 | breqtrrd 4681 |
1
⊢ (𝜑 → if((√‘𝐴) ∈ ℕ, 1, 0) ≤
(𝐹‘𝐴)) |