| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fvexd 6921 | . . 3
⊢ (𝜑 →
(Unit‘(ℤ/nℤ‘𝑅)) ∈ V) | 
| 2 |  | aks6d1c4.4 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 ∈ ℕ) | 
| 3 | 2 | nnnn0d 12587 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈
ℕ0) | 
| 4 |  | eqid 2737 | . . . . . . . . . . . 12
⊢
(ℤ/nℤ‘𝑅) = (ℤ/nℤ‘𝑅) | 
| 5 | 4 | zncrng 21563 | . . . . . . . . . . 11
⊢ (𝑅 ∈ ℕ0
→ (ℤ/nℤ‘𝑅) ∈ CRing) | 
| 6 | 3, 5 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 →
(ℤ/nℤ‘𝑅) ∈ CRing) | 
| 7 |  | crngring 20242 | . . . . . . . . . 10
⊢
((ℤ/nℤ‘𝑅) ∈ CRing →
(ℤ/nℤ‘𝑅) ∈ Ring) | 
| 8 |  | aks6d1c4.7 | . . . . . . . . . . 11
⊢ 𝐿 =
(ℤRHom‘(ℤ/nℤ‘𝑅)) | 
| 9 | 8 | zrhrhm 21522 | . . . . . . . . . 10
⊢
((ℤ/nℤ‘𝑅) ∈ Ring → 𝐿 ∈ (ℤring RingHom
(ℤ/nℤ‘𝑅))) | 
| 10 |  | zringbas 21464 | . . . . . . . . . . 11
⊢ ℤ =
(Base‘ℤring) | 
| 11 |  | eqid 2737 | . . . . . . . . . . 11
⊢
(Base‘(ℤ/nℤ‘𝑅)) =
(Base‘(ℤ/nℤ‘𝑅)) | 
| 12 | 10, 11 | rhmf 20485 | . . . . . . . . . 10
⊢ (𝐿 ∈ (ℤring
RingHom (ℤ/nℤ‘𝑅)) → 𝐿:ℤ⟶(Base‘(ℤ/nℤ‘𝑅))) | 
| 13 | 6, 7, 9, 12 | 4syl 19 | . . . . . . . . 9
⊢ (𝜑 → 𝐿:ℤ⟶(Base‘(ℤ/nℤ‘𝑅))) | 
| 14 | 13 | ffund 6740 | . . . . . . . 8
⊢ (𝜑 → Fun 𝐿) | 
| 15 | 14 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) → Fun 𝐿) | 
| 16 |  | simpr 484 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) → 𝑎 ∈ (𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) | 
| 17 |  | fvelima 6974 | . . . . . . 7
⊢ ((Fun
𝐿 ∧ 𝑎 ∈ (𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) → ∃𝑏 ∈ (𝐸 “ (ℕ0 ×
ℕ0))(𝐿‘𝑏) = 𝑎) | 
| 18 | 15, 16, 17 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ (𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) → ∃𝑏 ∈ (𝐸 “ (ℕ0 ×
ℕ0))(𝐿‘𝑏) = 𝑎) | 
| 19 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ ∃𝑏 ∈ (𝐸 “ (ℕ0 ×
ℕ0))(𝐿‘𝑏) = 𝑎) ∧ 𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) ∧ (𝐿‘𝑐) = 𝑎) → (𝐿‘𝑐) = 𝑎) | 
| 20 | 19 | eqcomd 2743 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ ∃𝑏 ∈ (𝐸 “ (ℕ0 ×
ℕ0))(𝐿‘𝑏) = 𝑎) ∧ 𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) ∧ (𝐿‘𝑐) = 𝑎) → 𝑎 = (𝐿‘𝑐)) | 
| 21 |  | simpll 767 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ∃𝑏 ∈ (𝐸 “ (ℕ0 ×
ℕ0))(𝐿‘𝑏) = 𝑎) ∧ 𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) → 𝜑) | 
| 22 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ∃𝑏 ∈ (𝐸 “ (ℕ0 ×
ℕ0))(𝐿‘𝑏) = 𝑎) ∧ 𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) → 𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) | 
| 23 | 21, 22 | jca 511 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∃𝑏 ∈ (𝐸 “ (ℕ0 ×
ℕ0))(𝐿‘𝑏) = 𝑎) ∧ 𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) → (𝜑 ∧ 𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0)))) | 
| 24 |  | ovexd 7466 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ0 ×
ℕ0)) → ((𝑃↑(1st ‘𝑚)) · ((𝑁 / 𝑃)↑(2nd ‘𝑚))) ∈ V) | 
| 25 |  | aks6d1c4.6 | . . . . . . . . . . . . . . . . . . . 20
⊢ 𝐸 = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0
↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙))) | 
| 26 |  | vex 3484 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝑘 ∈ V | 
| 27 |  | vex 3484 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝑙 ∈ V | 
| 28 | 26, 27 | op1std 8024 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑚 = 〈𝑘, 𝑙〉 → (1st ‘𝑚) = 𝑘) | 
| 29 | 28 | oveq2d 7447 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 = 〈𝑘, 𝑙〉 → (𝑃↑(1st ‘𝑚)) = (𝑃↑𝑘)) | 
| 30 | 26, 27 | op2ndd 8025 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑚 = 〈𝑘, 𝑙〉 → (2nd ‘𝑚) = 𝑙) | 
| 31 | 30 | oveq2d 7447 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 = 〈𝑘, 𝑙〉 → ((𝑁 / 𝑃)↑(2nd ‘𝑚)) = ((𝑁 / 𝑃)↑𝑙)) | 
| 32 | 29, 31 | oveq12d 7449 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 = 〈𝑘, 𝑙〉 → ((𝑃↑(1st ‘𝑚)) · ((𝑁 / 𝑃)↑(2nd ‘𝑚))) = ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙))) | 
| 33 | 32 | mpompt 7547 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 ∈ (ℕ0
× ℕ0) ↦ ((𝑃↑(1st ‘𝑚)) · ((𝑁 / 𝑃)↑(2nd ‘𝑚)))) = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0
↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙))) | 
| 34 | 33 | eqcomi 2746 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ ℕ0,
𝑙 ∈
ℕ0 ↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙))) = (𝑚 ∈ (ℕ0 ×
ℕ0) ↦ ((𝑃↑(1st ‘𝑚)) · ((𝑁 / 𝑃)↑(2nd ‘𝑚)))) | 
| 35 | 25, 34 | eqtri 2765 | . . . . . . . . . . . . . . . . . . 19
⊢ 𝐸 = (𝑚 ∈ (ℕ0 ×
ℕ0) ↦ ((𝑃↑(1st ‘𝑚)) · ((𝑁 / 𝑃)↑(2nd ‘𝑚)))) | 
| 36 | 24, 35 | fmptd 7134 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐸:(ℕ0 ×
ℕ0)⟶V) | 
| 37 | 36 | ffund 6740 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → Fun 𝐸) | 
| 38 | 37 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) → Fun 𝐸) | 
| 39 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) → 𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) | 
| 40 |  | fvelima 6974 | . . . . . . . . . . . . . . . 16
⊢ ((Fun
𝐸 ∧ 𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) → ∃𝑑 ∈ (ℕ0 ×
ℕ0)(𝐸‘𝑑) = 𝑐) | 
| 41 | 38, 39, 40 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) → ∃𝑑 ∈ (ℕ0 ×
ℕ0)(𝐸‘𝑑) = 𝑐) | 
| 42 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) ∧ ∃𝑑 ∈ (ℕ0 ×
ℕ0)(𝐸‘𝑑) = 𝑐) ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ (𝐸‘𝑒) = 𝑐) → (𝐸‘𝑒) = 𝑐) | 
| 43 | 42 | eqcomd 2743 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) ∧ ∃𝑑 ∈ (ℕ0 ×
ℕ0)(𝐸‘𝑑) = 𝑐) ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ (𝐸‘𝑒) = 𝑐) → 𝑐 = (𝐸‘𝑒)) | 
| 44 | 43 | oveq1d 7446 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) ∧ ∃𝑑 ∈ (ℕ0 ×
ℕ0)(𝐸‘𝑑) = 𝑐) ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ (𝐸‘𝑒) = 𝑐) → (𝑐 gcd 𝑅) = ((𝐸‘𝑒) gcd 𝑅)) | 
| 45 |  | simplll 775 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) ∧ ∃𝑑 ∈ (ℕ0 ×
ℕ0)(𝐸‘𝑑) = 𝑐) ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) → 𝜑) | 
| 46 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) ∧ ∃𝑑 ∈ (ℕ0 ×
ℕ0)(𝐸‘𝑑) = 𝑐) ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) → 𝑒 ∈ (ℕ0 ×
ℕ0)) | 
| 47 | 45, 46 | jca 511 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) ∧ ∃𝑑 ∈ (ℕ0 ×
ℕ0)(𝐸‘𝑑) = 𝑐) ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) → (𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0))) | 
| 48 | 35 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) → 𝐸 = (𝑚 ∈ (ℕ0 ×
ℕ0) ↦ ((𝑃↑(1st ‘𝑚)) · ((𝑁 / 𝑃)↑(2nd ‘𝑚))))) | 
| 49 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ 𝑚 = 𝑒) → 𝑚 = 𝑒) | 
| 50 | 49 | fveq2d 6910 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ 𝑚 = 𝑒) → (1st ‘𝑚) = (1st ‘𝑒)) | 
| 51 | 50 | oveq2d 7447 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ 𝑚 = 𝑒) → (𝑃↑(1st ‘𝑚)) = (𝑃↑(1st ‘𝑒))) | 
| 52 | 49 | fveq2d 6910 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ 𝑚 = 𝑒) → (2nd ‘𝑚) = (2nd ‘𝑒)) | 
| 53 | 52 | oveq2d 7447 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ 𝑚 = 𝑒) → ((𝑁 / 𝑃)↑(2nd ‘𝑚)) = ((𝑁 / 𝑃)↑(2nd ‘𝑒))) | 
| 54 | 51, 53 | oveq12d 7449 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ 𝑚 = 𝑒) → ((𝑃↑(1st ‘𝑚)) · ((𝑁 / 𝑃)↑(2nd ‘𝑚))) = ((𝑃↑(1st ‘𝑒)) · ((𝑁 / 𝑃)↑(2nd ‘𝑒)))) | 
| 55 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) → 𝑒 ∈ (ℕ0 ×
ℕ0)) | 
| 56 |  | ovexd 7466 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) → ((𝑃↑(1st ‘𝑒)) · ((𝑁 / 𝑃)↑(2nd ‘𝑒))) ∈ V) | 
| 57 | 48, 54, 55, 56 | fvmptd 7023 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) → (𝐸‘𝑒) = ((𝑃↑(1st ‘𝑒)) · ((𝑁 / 𝑃)↑(2nd ‘𝑒)))) | 
| 58 |  | aks6d1c4.2 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝑃 ∈ ℙ) | 
| 59 |  | prmnn 16711 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) | 
| 60 | 58, 59 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝑃 ∈ ℕ) | 
| 61 | 60 | nnzd 12640 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝑃 ∈ ℤ) | 
| 62 | 61 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) → 𝑃 ∈ ℤ) | 
| 63 |  | xp1st 8046 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑒 ∈ (ℕ0
× ℕ0) → (1st ‘𝑒) ∈
ℕ0) | 
| 64 | 63 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) → (1st ‘𝑒) ∈
ℕ0) | 
| 65 | 62, 64 | zexpcld 14128 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) → (𝑃↑(1st ‘𝑒)) ∈
ℤ) | 
| 66 |  | aks6d1c4.3 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝑃 ∥ 𝑁) | 
| 67 | 60 | nnne0d 12316 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝑃 ≠ 0) | 
| 68 |  | aks6d1c4.1 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 69 | 68 | nnzd 12640 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝑁 ∈ ℤ) | 
| 70 |  | dvdsval2 16293 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑃 ∈ ℤ ∧ 𝑃 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝑃 ∥ 𝑁 ↔ (𝑁 / 𝑃) ∈ ℤ)) | 
| 71 | 61, 67, 69, 70 | syl3anc 1373 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (𝑃 ∥ 𝑁 ↔ (𝑁 / 𝑃) ∈ ℤ)) | 
| 72 | 66, 71 | mpbid 232 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝑁 / 𝑃) ∈ ℤ) | 
| 73 | 72 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) → (𝑁 / 𝑃) ∈ ℤ) | 
| 74 |  | xp2nd 8047 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑒 ∈ (ℕ0
× ℕ0) → (2nd ‘𝑒) ∈
ℕ0) | 
| 75 | 74 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) → (2nd ‘𝑒) ∈
ℕ0) | 
| 76 | 73, 75 | zexpcld 14128 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) → ((𝑁 / 𝑃)↑(2nd ‘𝑒)) ∈
ℤ) | 
| 77 | 65, 76 | zmulcld 12728 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) → ((𝑃↑(1st ‘𝑒)) · ((𝑁 / 𝑃)↑(2nd ‘𝑒))) ∈
ℤ) | 
| 78 | 57, 77 | eqeltrd 2841 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) → (𝐸‘𝑒) ∈ ℤ) | 
| 79 | 57 | oveq1d 7446 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) → ((𝐸‘𝑒) gcd 𝑅) = (((𝑃↑(1st ‘𝑒)) · ((𝑁 / 𝑃)↑(2nd ‘𝑒))) gcd 𝑅)) | 
| 80 | 2 | nnzd 12640 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝑅 ∈ ℤ) | 
| 81 | 80 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) → 𝑅 ∈ ℤ) | 
| 82 | 77, 81 | gcdcomd 16551 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) → (((𝑃↑(1st ‘𝑒)) · ((𝑁 / 𝑃)↑(2nd ‘𝑒))) gcd 𝑅) = (𝑅 gcd ((𝑃↑(1st ‘𝑒)) · ((𝑁 / 𝑃)↑(2nd ‘𝑒))))) | 
| 83 | 80, 61, 69 | 3jca 1129 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝜑 → (𝑅 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ)) | 
| 84 |  | aks6d1c4.5 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) | 
| 85 | 69, 80 | jca 511 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝜑 → (𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ)) | 
| 86 |  | gcdcom 16550 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ) → (𝑁 gcd 𝑅) = (𝑅 gcd 𝑁)) | 
| 87 | 85, 86 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝜑 → (𝑁 gcd 𝑅) = (𝑅 gcd 𝑁)) | 
| 88 |  | eqeq1 2741 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑁 gcd 𝑅) = (𝑅 gcd 𝑁) → ((𝑁 gcd 𝑅) = 1 ↔ (𝑅 gcd 𝑁) = 1)) | 
| 89 | 87, 88 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 → ((𝑁 gcd 𝑅) = 1 ↔ (𝑅 gcd 𝑁) = 1)) | 
| 90 | 89 | pm5.74i 271 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 → (𝑁 gcd 𝑅) = 1) ↔ (𝜑 → (𝑅 gcd 𝑁) = 1)) | 
| 91 | 84, 90 | mpbi 230 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → (𝑅 gcd 𝑁) = 1) | 
| 92 | 91, 66 | jca 511 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝜑 → ((𝑅 gcd 𝑁) = 1 ∧ 𝑃 ∥ 𝑁)) | 
| 93 |  | rpdvds 16697 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑅 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑅 gcd 𝑁) = 1 ∧ 𝑃 ∥ 𝑁)) → (𝑅 gcd 𝑃) = 1) | 
| 94 | 83, 92, 93 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝜑 → (𝑅 gcd 𝑃) = 1) | 
| 95 | 94 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) → (𝑅 gcd 𝑃) = 1) | 
| 96 | 95 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ (1st ‘𝑒) ∈ ℕ) → (𝑅 gcd 𝑃) = 1) | 
| 97 | 2 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ (1st ‘𝑒) ∈ ℕ) → 𝑅 ∈ ℕ) | 
| 98 | 60 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ (1st ‘𝑒) ∈ ℕ) → 𝑃 ∈ ℕ) | 
| 99 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ (1st ‘𝑒) ∈ ℕ) → (1st
‘𝑒) ∈
ℕ) | 
| 100 |  | rprpwr 16596 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑅 ∈ ℕ ∧ 𝑃 ∈ ℕ ∧
(1st ‘𝑒)
∈ ℕ) → ((𝑅
gcd 𝑃) = 1 → (𝑅 gcd (𝑃↑(1st ‘𝑒))) = 1)) | 
| 101 | 97, 98, 99, 100 | syl3anc 1373 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ (1st ‘𝑒) ∈ ℕ) → ((𝑅 gcd 𝑃) = 1 → (𝑅 gcd (𝑃↑(1st ‘𝑒))) = 1)) | 
| 102 | 96, 101 | mpd 15 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ (1st ‘𝑒) ∈ ℕ) → (𝑅 gcd (𝑃↑(1st ‘𝑒))) = 1) | 
| 103 | 64 | anim1i 615 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ (1st ‘𝑒) ≠ 0) → ((1st
‘𝑒) ∈
ℕ0 ∧ (1st ‘𝑒) ≠ 0)) | 
| 104 |  | elnnne0 12540 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((1st ‘𝑒) ∈ ℕ ↔ ((1st
‘𝑒) ∈
ℕ0 ∧ (1st ‘𝑒) ≠ 0)) | 
| 105 | 103, 104 | sylibr 234 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ (1st ‘𝑒) ≠ 0) → (1st ‘𝑒) ∈
ℕ) | 
| 106 | 105 | ex 412 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) → ((1st ‘𝑒) ≠ 0 → (1st ‘𝑒) ∈
ℕ)) | 
| 107 | 106 | necon1bd 2958 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) → (¬ (1st ‘𝑒) ∈ ℕ → (1st
‘𝑒) =
0)) | 
| 108 | 107 | imp 406 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ ¬ (1st ‘𝑒) ∈ ℕ) → (1st
‘𝑒) =
0) | 
| 109 | 108 | oveq2d 7447 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ ¬ (1st ‘𝑒) ∈ ℕ) → (𝑃↑(1st ‘𝑒)) = (𝑃↑0)) | 
| 110 | 109 | oveq2d 7447 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ ¬ (1st ‘𝑒) ∈ ℕ) → (𝑅 gcd (𝑃↑(1st ‘𝑒))) = (𝑅 gcd (𝑃↑0))) | 
| 111 | 62 | zcnd 12723 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) → 𝑃 ∈ ℂ) | 
| 112 | 111 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ ¬ (1st ‘𝑒) ∈ ℕ) → 𝑃 ∈ ℂ) | 
| 113 | 112 | exp0d 14180 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ ¬ (1st ‘𝑒) ∈ ℕ) → (𝑃↑0) = 1) | 
| 114 | 113 | oveq2d 7447 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ ¬ (1st ‘𝑒) ∈ ℕ) → (𝑅 gcd (𝑃↑0)) = (𝑅 gcd 1)) | 
| 115 | 81 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ ¬ (1st ‘𝑒) ∈ ℕ) → 𝑅 ∈ ℤ) | 
| 116 |  | gcd1 16565 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑅 ∈ ℤ → (𝑅 gcd 1) = 1) | 
| 117 | 115, 116 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ ¬ (1st ‘𝑒) ∈ ℕ) → (𝑅 gcd 1) = 1) | 
| 118 | 114, 117 | eqtrd 2777 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ ¬ (1st ‘𝑒) ∈ ℕ) → (𝑅 gcd (𝑃↑0)) = 1) | 
| 119 | 110, 118 | eqtrd 2777 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ ¬ (1st ‘𝑒) ∈ ℕ) → (𝑅 gcd (𝑃↑(1st ‘𝑒))) = 1) | 
| 120 | 102, 119 | pm2.61dan 813 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) → (𝑅 gcd (𝑃↑(1st ‘𝑒))) = 1) | 
| 121 | 80, 72, 69 | 3jca 1129 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝜑 → (𝑅 ∈ ℤ ∧ (𝑁 / 𝑃) ∈ ℤ ∧ 𝑁 ∈ ℤ)) | 
| 122 | 68 | nnred 12281 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝜑 → 𝑁 ∈ ℝ) | 
| 123 | 122 | recnd 11289 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝜑 → 𝑁 ∈ ℂ) | 
| 124 | 60 | nnred 12281 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝜑 → 𝑃 ∈ ℝ) | 
| 125 | 124 | recnd 11289 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝜑 → 𝑃 ∈ ℂ) | 
| 126 | 68 | nngt0d 12315 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝜑 → 0 < 𝑁) | 
| 127 | 126 | gt0ne0d 11827 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝜑 → 𝑁 ≠ 0) | 
| 128 | 123, 125,
127, 67 | ddcand 12063 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 → (𝑁 / (𝑁 / 𝑃)) = 𝑃) | 
| 129 | 128, 61 | eqeltrd 2841 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝜑 → (𝑁 / (𝑁 / 𝑃)) ∈ ℤ) | 
| 130 | 60 | nngt0d 12315 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝜑 → 0 < 𝑃) | 
| 131 | 122, 124,
126, 130 | divgt0d 12203 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝜑 → 0 < (𝑁 / 𝑃)) | 
| 132 | 131 | gt0ne0d 11827 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 → (𝑁 / 𝑃) ≠ 0) | 
| 133 |  | dvdsval2 16293 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝑁 / 𝑃) ∈ ℤ ∧ (𝑁 / 𝑃) ≠ 0 ∧ 𝑁 ∈ ℤ) → ((𝑁 / 𝑃) ∥ 𝑁 ↔ (𝑁 / (𝑁 / 𝑃)) ∈ ℤ)) | 
| 134 | 72, 132, 69, 133 | syl3anc 1373 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝜑 → ((𝑁 / 𝑃) ∥ 𝑁 ↔ (𝑁 / (𝑁 / 𝑃)) ∈ ℤ)) | 
| 135 | 129, 134 | mpbird 257 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → (𝑁 / 𝑃) ∥ 𝑁) | 
| 136 | 91, 135 | jca 511 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝜑 → ((𝑅 gcd 𝑁) = 1 ∧ (𝑁 / 𝑃) ∥ 𝑁)) | 
| 137 |  | rpdvds 16697 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑅 ∈ ℤ ∧ (𝑁 / 𝑃) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑅 gcd 𝑁) = 1 ∧ (𝑁 / 𝑃) ∥ 𝑁)) → (𝑅 gcd (𝑁 / 𝑃)) = 1) | 
| 138 | 121, 136,
137 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝜑 → (𝑅 gcd (𝑁 / 𝑃)) = 1) | 
| 139 | 138 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) → (𝑅 gcd (𝑁 / 𝑃)) = 1) | 
| 140 | 139 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ (2nd ‘𝑒) ∈ ℕ) → (𝑅 gcd (𝑁 / 𝑃)) = 1) | 
| 141 | 2 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ (2nd ‘𝑒) ∈ ℕ) → 𝑅 ∈ ℕ) | 
| 142 | 72, 131 | jca 511 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → ((𝑁 / 𝑃) ∈ ℤ ∧ 0 < (𝑁 / 𝑃))) | 
| 143 |  | elnnz 12623 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑁 / 𝑃) ∈ ℕ ↔ ((𝑁 / 𝑃) ∈ ℤ ∧ 0 < (𝑁 / 𝑃))) | 
| 144 | 142, 143 | sylibr 234 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝜑 → (𝑁 / 𝑃) ∈ ℕ) | 
| 145 | 144 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) → (𝑁 / 𝑃) ∈ ℕ) | 
| 146 | 145 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ (2nd ‘𝑒) ∈ ℕ) → (𝑁 / 𝑃) ∈ ℕ) | 
| 147 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ (2nd ‘𝑒) ∈ ℕ) → (2nd
‘𝑒) ∈
ℕ) | 
| 148 |  | rprpwr 16596 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑅 ∈ ℕ ∧ (𝑁 / 𝑃) ∈ ℕ ∧ (2nd
‘𝑒) ∈ ℕ)
→ ((𝑅 gcd (𝑁 / 𝑃)) = 1 → (𝑅 gcd ((𝑁 / 𝑃)↑(2nd ‘𝑒))) = 1)) | 
| 149 | 141, 146,
147, 148 | syl3anc 1373 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ (2nd ‘𝑒) ∈ ℕ) → ((𝑅 gcd (𝑁 / 𝑃)) = 1 → (𝑅 gcd ((𝑁 / 𝑃)↑(2nd ‘𝑒))) = 1)) | 
| 150 | 140, 149 | mpd 15 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ (2nd ‘𝑒) ∈ ℕ) → (𝑅 gcd ((𝑁 / 𝑃)↑(2nd ‘𝑒))) = 1) | 
| 151 | 75 | anim1i 615 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ (2nd ‘𝑒) ≠ 0) → ((2nd
‘𝑒) ∈
ℕ0 ∧ (2nd ‘𝑒) ≠ 0)) | 
| 152 |  | elnnne0 12540 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((2nd ‘𝑒) ∈ ℕ ↔ ((2nd
‘𝑒) ∈
ℕ0 ∧ (2nd ‘𝑒) ≠ 0)) | 
| 153 | 151, 152 | sylibr 234 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ (2nd ‘𝑒) ≠ 0) → (2nd ‘𝑒) ∈
ℕ) | 
| 154 | 153 | ex 412 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) → ((2nd ‘𝑒) ≠ 0 → (2nd ‘𝑒) ∈
ℕ)) | 
| 155 | 154 | necon1bd 2958 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) → (¬ (2nd ‘𝑒) ∈ ℕ → (2nd
‘𝑒) =
0)) | 
| 156 | 155 | imp 406 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ ¬ (2nd ‘𝑒) ∈ ℕ) → (2nd
‘𝑒) =
0) | 
| 157 | 156 | oveq2d 7447 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ ¬ (2nd ‘𝑒) ∈ ℕ) → ((𝑁 / 𝑃)↑(2nd ‘𝑒)) = ((𝑁 / 𝑃)↑0)) | 
| 158 | 157 | oveq2d 7447 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ ¬ (2nd ‘𝑒) ∈ ℕ) → (𝑅 gcd ((𝑁 / 𝑃)↑(2nd ‘𝑒))) = (𝑅 gcd ((𝑁 / 𝑃)↑0))) | 
| 159 | 123 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) → 𝑁 ∈ ℂ) | 
| 160 | 159 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ ¬ (2nd ‘𝑒) ∈ ℕ) → 𝑁 ∈ ℂ) | 
| 161 | 111 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ ¬ (2nd ‘𝑒) ∈ ℕ) → 𝑃 ∈ ℂ) | 
| 162 | 67 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ ¬ (2nd ‘𝑒) ∈ ℕ) → 𝑃 ≠ 0) | 
| 163 | 160, 161,
162 | divcld 12043 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ ¬ (2nd ‘𝑒) ∈ ℕ) → (𝑁 / 𝑃) ∈ ℂ) | 
| 164 | 163 | exp0d 14180 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ ¬ (2nd ‘𝑒) ∈ ℕ) → ((𝑁 / 𝑃)↑0) = 1) | 
| 165 | 164 | oveq2d 7447 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ ¬ (2nd ‘𝑒) ∈ ℕ) → (𝑅 gcd ((𝑁 / 𝑃)↑0)) = (𝑅 gcd 1)) | 
| 166 | 158, 165 | eqtrd 2777 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ ¬ (2nd ‘𝑒) ∈ ℕ) → (𝑅 gcd ((𝑁 / 𝑃)↑(2nd ‘𝑒))) = (𝑅 gcd 1)) | 
| 167 | 81 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ ¬ (2nd ‘𝑒) ∈ ℕ) → 𝑅 ∈ ℤ) | 
| 168 | 167, 116 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ ¬ (2nd ‘𝑒) ∈ ℕ) → (𝑅 gcd 1) = 1) | 
| 169 | 166, 168 | eqtrd 2777 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ ¬ (2nd ‘𝑒) ∈ ℕ) → (𝑅 gcd ((𝑁 / 𝑃)↑(2nd ‘𝑒))) = 1) | 
| 170 | 150, 169 | pm2.61dan 813 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) → (𝑅 gcd ((𝑁 / 𝑃)↑(2nd ‘𝑒))) = 1) | 
| 171 | 120, 170 | jca 511 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) → ((𝑅 gcd (𝑃↑(1st ‘𝑒))) = 1 ∧ (𝑅 gcd ((𝑁 / 𝑃)↑(2nd ‘𝑒))) = 1)) | 
| 172 |  | rpmul 16696 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑅 ∈ ℤ ∧ (𝑃↑(1st
‘𝑒)) ∈ ℤ
∧ ((𝑁 / 𝑃)↑(2nd
‘𝑒)) ∈ ℤ)
→ (((𝑅 gcd (𝑃↑(1st
‘𝑒))) = 1 ∧
(𝑅 gcd ((𝑁 / 𝑃)↑(2nd ‘𝑒))) = 1) → (𝑅 gcd ((𝑃↑(1st ‘𝑒)) · ((𝑁 / 𝑃)↑(2nd ‘𝑒)))) = 1)) | 
| 173 | 81, 65, 76, 172 | syl3anc 1373 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) → (((𝑅 gcd (𝑃↑(1st ‘𝑒))) = 1 ∧ (𝑅 gcd ((𝑁 / 𝑃)↑(2nd ‘𝑒))) = 1) → (𝑅 gcd ((𝑃↑(1st ‘𝑒)) · ((𝑁 / 𝑃)↑(2nd ‘𝑒)))) = 1)) | 
| 174 | 171, 173 | mpd 15 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) → (𝑅 gcd ((𝑃↑(1st ‘𝑒)) · ((𝑁 / 𝑃)↑(2nd ‘𝑒)))) = 1) | 
| 175 | 82, 174 | eqtrd 2777 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) → (((𝑃↑(1st ‘𝑒)) · ((𝑁 / 𝑃)↑(2nd ‘𝑒))) gcd 𝑅) = 1) | 
| 176 | 79, 175 | eqtrd 2777 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) → ((𝐸‘𝑒) gcd 𝑅) = 1) | 
| 177 | 78, 176 | jca 511 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) → ((𝐸‘𝑒) ∈ ℤ ∧ ((𝐸‘𝑒) gcd 𝑅) = 1)) | 
| 178 | 47, 177 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) ∧ ∃𝑑 ∈ (ℕ0 ×
ℕ0)(𝐸‘𝑑) = 𝑐) ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) → ((𝐸‘𝑒) ∈ ℤ ∧ ((𝐸‘𝑒) gcd 𝑅) = 1)) | 
| 179 | 178 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) ∧ ∃𝑑 ∈ (ℕ0 ×
ℕ0)(𝐸‘𝑑) = 𝑐) ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ (𝐸‘𝑒) = 𝑐) → ((𝐸‘𝑒) ∈ ℤ ∧ ((𝐸‘𝑒) gcd 𝑅) = 1)) | 
| 180 | 179 | simprd 495 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) ∧ ∃𝑑 ∈ (ℕ0 ×
ℕ0)(𝐸‘𝑑) = 𝑐) ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ (𝐸‘𝑒) = 𝑐) → ((𝐸‘𝑒) gcd 𝑅) = 1) | 
| 181 | 44, 180 | eqtrd 2777 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) ∧ ∃𝑑 ∈ (ℕ0 ×
ℕ0)(𝐸‘𝑑) = 𝑐) ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ (𝐸‘𝑒) = 𝑐) → (𝑐 gcd 𝑅) = 1) | 
| 182 | 179 | simpld 494 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) ∧ ∃𝑑 ∈ (ℕ0 ×
ℕ0)(𝐸‘𝑑) = 𝑐) ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ (𝐸‘𝑒) = 𝑐) → (𝐸‘𝑒) ∈ ℤ) | 
| 183 | 43, 182 | eqeltrd 2841 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) ∧ ∃𝑑 ∈ (ℕ0 ×
ℕ0)(𝐸‘𝑑) = 𝑐) ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ (𝐸‘𝑒) = 𝑐) → 𝑐 ∈ ℤ) | 
| 184 | 181, 183 | jca 511 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) ∧ ∃𝑑 ∈ (ℕ0 ×
ℕ0)(𝐸‘𝑑) = 𝑐) ∧ 𝑒 ∈ (ℕ0 ×
ℕ0)) ∧ (𝐸‘𝑒) = 𝑐) → ((𝑐 gcd 𝑅) = 1 ∧ 𝑐 ∈ ℤ)) | 
| 185 |  | nfv 1914 | . . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑒(𝐸‘𝑑) = 𝑐 | 
| 186 |  | nfv 1914 | . . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑑(𝐸‘𝑒) = 𝑐 | 
| 187 |  | fveqeq2 6915 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑑 = 𝑒 → ((𝐸‘𝑑) = 𝑐 ↔ (𝐸‘𝑒) = 𝑐)) | 
| 188 | 185, 186,
187 | cbvrexw 3307 | . . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑑 ∈
(ℕ0 × ℕ0)(𝐸‘𝑑) = 𝑐 ↔ ∃𝑒 ∈ (ℕ0 ×
ℕ0)(𝐸‘𝑒) = 𝑐) | 
| 189 | 188 | biimpi 216 | . . . . . . . . . . . . . . . . . 18
⊢
(∃𝑑 ∈
(ℕ0 × ℕ0)(𝐸‘𝑑) = 𝑐 → ∃𝑒 ∈ (ℕ0 ×
ℕ0)(𝐸‘𝑒) = 𝑐) | 
| 190 | 189 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) ∧ ∃𝑑 ∈ (ℕ0 ×
ℕ0)(𝐸‘𝑑) = 𝑐) → ∃𝑒 ∈ (ℕ0 ×
ℕ0)(𝐸‘𝑒) = 𝑐) | 
| 191 | 184, 190 | r19.29a 3162 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) ∧ ∃𝑑 ∈ (ℕ0 ×
ℕ0)(𝐸‘𝑑) = 𝑐) → ((𝑐 gcd 𝑅) = 1 ∧ 𝑐 ∈ ℤ)) | 
| 192 | 191 | ex 412 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) → (∃𝑑 ∈ (ℕ0 ×
ℕ0)(𝐸‘𝑑) = 𝑐 → ((𝑐 gcd 𝑅) = 1 ∧ 𝑐 ∈ ℤ))) | 
| 193 | 41, 192 | mpd 15 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) → ((𝑐 gcd 𝑅) = 1 ∧ 𝑐 ∈ ℤ)) | 
| 194 | 193 | simpld 494 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) → (𝑐 gcd 𝑅) = 1) | 
| 195 | 3 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) → 𝑅 ∈
ℕ0) | 
| 196 | 193 | simprd 495 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) → 𝑐 ∈ ℤ) | 
| 197 |  | eqid 2737 | . . . . . . . . . . . . . . 15
⊢
(Unit‘(ℤ/nℤ‘𝑅)) =
(Unit‘(ℤ/nℤ‘𝑅)) | 
| 198 | 4, 197, 8 | znunit 21582 | . . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℕ0
∧ 𝑐 ∈ ℤ)
→ ((𝐿‘𝑐) ∈
(Unit‘(ℤ/nℤ‘𝑅)) ↔ (𝑐 gcd 𝑅) = 1)) | 
| 199 | 195, 196,
198 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) → ((𝐿‘𝑐) ∈
(Unit‘(ℤ/nℤ‘𝑅)) ↔ (𝑐 gcd 𝑅) = 1)) | 
| 200 | 194, 199 | mpbird 257 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) → (𝐿‘𝑐) ∈
(Unit‘(ℤ/nℤ‘𝑅))) | 
| 201 | 23, 200 | syl 17 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ ∃𝑏 ∈ (𝐸 “ (ℕ0 ×
ℕ0))(𝐿‘𝑏) = 𝑎) ∧ 𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) → (𝐿‘𝑐) ∈
(Unit‘(ℤ/nℤ‘𝑅))) | 
| 202 | 201 | adantr 480 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ ∃𝑏 ∈ (𝐸 “ (ℕ0 ×
ℕ0))(𝐿‘𝑏) = 𝑎) ∧ 𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) ∧ (𝐿‘𝑐) = 𝑎) → (𝐿‘𝑐) ∈
(Unit‘(ℤ/nℤ‘𝑅))) | 
| 203 | 20, 202 | eqeltrd 2841 | . . . . . . . . 9
⊢ ((((𝜑 ∧ ∃𝑏 ∈ (𝐸 “ (ℕ0 ×
ℕ0))(𝐿‘𝑏) = 𝑎) ∧ 𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) ∧ (𝐿‘𝑐) = 𝑎) → 𝑎 ∈
(Unit‘(ℤ/nℤ‘𝑅))) | 
| 204 |  | nfv 1914 | . . . . . . . . . . . 12
⊢
Ⅎ𝑐(𝐿‘𝑏) = 𝑎 | 
| 205 |  | nfv 1914 | . . . . . . . . . . . 12
⊢
Ⅎ𝑏(𝐿‘𝑐) = 𝑎 | 
| 206 |  | fveqeq2 6915 | . . . . . . . . . . . 12
⊢ (𝑏 = 𝑐 → ((𝐿‘𝑏) = 𝑎 ↔ (𝐿‘𝑐) = 𝑎)) | 
| 207 | 204, 205,
206 | cbvrexw 3307 | . . . . . . . . . . 11
⊢
(∃𝑏 ∈
(𝐸 “
(ℕ0 × ℕ0))(𝐿‘𝑏) = 𝑎 ↔ ∃𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))(𝐿‘𝑐) = 𝑎) | 
| 208 | 207 | biimpi 216 | . . . . . . . . . 10
⊢
(∃𝑏 ∈
(𝐸 “
(ℕ0 × ℕ0))(𝐿‘𝑏) = 𝑎 → ∃𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))(𝐿‘𝑐) = 𝑎) | 
| 209 | 208 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ ∃𝑏 ∈ (𝐸 “ (ℕ0 ×
ℕ0))(𝐿‘𝑏) = 𝑎) → ∃𝑐 ∈ (𝐸 “ (ℕ0 ×
ℕ0))(𝐿‘𝑐) = 𝑎) | 
| 210 | 203, 209 | r19.29a 3162 | . . . . . . . 8
⊢ ((𝜑 ∧ ∃𝑏 ∈ (𝐸 “ (ℕ0 ×
ℕ0))(𝐿‘𝑏) = 𝑎) → 𝑎 ∈
(Unit‘(ℤ/nℤ‘𝑅))) | 
| 211 | 210 | ex 412 | . . . . . . 7
⊢ (𝜑 → (∃𝑏 ∈ (𝐸 “ (ℕ0 ×
ℕ0))(𝐿‘𝑏) = 𝑎 → 𝑎 ∈
(Unit‘(ℤ/nℤ‘𝑅)))) | 
| 212 | 211 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ (𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) → (∃𝑏 ∈ (𝐸 “ (ℕ0 ×
ℕ0))(𝐿‘𝑏) = 𝑎 → 𝑎 ∈
(Unit‘(ℤ/nℤ‘𝑅)))) | 
| 213 | 18, 212 | mpd 15 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) → 𝑎 ∈
(Unit‘(ℤ/nℤ‘𝑅))) | 
| 214 | 213 | ex 412 | . . . 4
⊢ (𝜑 → (𝑎 ∈ (𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))) → 𝑎 ∈
(Unit‘(ℤ/nℤ‘𝑅)))) | 
| 215 | 214 | ssrdv 3989 | . . 3
⊢ (𝜑 → (𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))) ⊆ (Unit‘(ℤ/nℤ‘𝑅))) | 
| 216 |  | hashss 14448 | . . 3
⊢
(((Unit‘(ℤ/nℤ‘𝑅)) ∈ V ∧ (𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))) ⊆ (Unit‘(ℤ/nℤ‘𝑅))) → (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) ≤
(♯‘(Unit‘(ℤ/nℤ‘𝑅)))) | 
| 217 | 1, 215, 216 | syl2anc 584 | . 2
⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) ≤
(♯‘(Unit‘(ℤ/nℤ‘𝑅)))) | 
| 218 | 4, 197 | znunithash 21583 | . . 3
⊢ (𝑅 ∈ ℕ →
(♯‘(Unit‘(ℤ/nℤ‘𝑅))) = (ϕ‘𝑅)) | 
| 219 | 2, 218 | syl 17 | . 2
⊢ (𝜑 →
(♯‘(Unit‘(ℤ/nℤ‘𝑅))) = (ϕ‘𝑅)) | 
| 220 | 217, 219 | breqtrd 5169 | 1
⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) ≤ (ϕ‘𝑅)) |