| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | aks6d1c1.21 | . . . . 5
⊢ (𝜑 → 𝐴 ∈
ℕ0) | 
| 2 | 1 | nn0zd 12641 | . . . 4
⊢ (𝜑 → 𝐴 ∈ ℤ) | 
| 3 | 1 | nn0ge0d 12592 | . . . 4
⊢ (𝜑 → 0 ≤ 𝐴) | 
| 4 | 1 | nn0red 12590 | . . . . 5
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 5 | 4 | leidd 11830 | . . . 4
⊢ (𝜑 → 𝐴 ≤ 𝐴) | 
| 6 | 2, 3, 5 | 3jca 1128 | . . 3
⊢ (𝜑 → (𝐴 ∈ ℤ ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐴)) | 
| 7 |  | oveq2 7440 | . . . . . . . 8
⊢ (ℎ = 0 → (0...ℎ) = (0...0)) | 
| 8 | 7 | mpteq1d 5236 | . . . . . . 7
⊢ (ℎ = 0 → (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑖 ∈ (0...0) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) | 
| 9 | 8 | oveq2d 7448 | . . . . . 6
⊢ (ℎ = 0 → (𝑊 Σg (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σg (𝑖 ∈ (0...0) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) | 
| 10 | 9 | breq2d 5154 | . . . . 5
⊢ (ℎ = 0 → (𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) ↔ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...0) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))) | 
| 11 |  | oveq2 7440 | . . . . . . . 8
⊢ (ℎ = 𝑗 → (0...ℎ) = (0...𝑗)) | 
| 12 | 11 | mpteq1d 5236 | . . . . . . 7
⊢ (ℎ = 𝑗 → (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) | 
| 13 | 12 | oveq2d 7448 | . . . . . 6
⊢ (ℎ = 𝑗 → (𝑊 Σg (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) | 
| 14 | 13 | breq2d 5154 | . . . . 5
⊢ (ℎ = 𝑗 → (𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) ↔ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))) | 
| 15 |  | oveq2 7440 | . . . . . . . 8
⊢ (ℎ = (𝑗 + 1) → (0...ℎ) = (0...(𝑗 + 1))) | 
| 16 | 15 | mpteq1d 5236 | . . . . . . 7
⊢ (ℎ = (𝑗 + 1) → (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) | 
| 17 | 16 | oveq2d 7448 | . . . . . 6
⊢ (ℎ = (𝑗 + 1) → (𝑊 Σg (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σg (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) | 
| 18 | 17 | breq2d 5154 | . . . . 5
⊢ (ℎ = (𝑗 + 1) → (𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) ↔ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))) | 
| 19 |  | oveq2 7440 | . . . . . . . 8
⊢ (ℎ = 𝐴 → (0...ℎ) = (0...𝐴)) | 
| 20 | 19 | mpteq1d 5236 | . . . . . . 7
⊢ (ℎ = 𝐴 → (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) | 
| 21 | 20 | oveq2d 7448 | . . . . . 6
⊢ (ℎ = 𝐴 → (𝑊 Σg (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σg (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) | 
| 22 | 21 | breq2d 5154 | . . . . 5
⊢ (ℎ = 𝐴 → (𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...ℎ) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) ↔ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))) | 
| 23 |  | aks6d1c1.1 | . . . . . . . 8
⊢  ∼ =
{〈𝑒, 𝑓〉 ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝑒 ↑ ((𝑂‘𝑓)‘𝑦)) = ((𝑂‘𝑓)‘(𝑒 ↑ 𝑦)))} | 
| 24 |  | aks6d1c1.2 | . . . . . . . 8
⊢ 𝑆 = (Poly1‘𝐾) | 
| 25 |  | aks6d1c1.3 | . . . . . . . 8
⊢ 𝐵 = (Base‘𝑆) | 
| 26 |  | aks6d1c1.4 | . . . . . . . 8
⊢ 𝑋 = (var1‘𝐾) | 
| 27 |  | aks6d1c1.5 | . . . . . . . 8
⊢ 𝑊 = (mulGrp‘𝑆) | 
| 28 |  | aks6d1c1.6 | . . . . . . . 8
⊢ 𝑉 = (mulGrp‘𝐾) | 
| 29 |  | aks6d1c1.7 | . . . . . . . 8
⊢  ↑ =
(.g‘𝑉) | 
| 30 |  | aks6d1c1.8 | . . . . . . . 8
⊢ 𝐶 = (algSc‘𝑆) | 
| 31 |  | aks6d1c1.9 | . . . . . . . 8
⊢ 𝐷 = (.g‘𝑊) | 
| 32 |  | aks6d1c1.10 | . . . . . . . 8
⊢ 𝑃 = (chr‘𝐾) | 
| 33 |  | aks6d1c1.11 | . . . . . . . 8
⊢ 𝑂 = (eval1‘𝐾) | 
| 34 |  | aks6d1c1.12 | . . . . . . . 8
⊢  + =
(+g‘𝑆) | 
| 35 |  | aks6d1c1.13 | . . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ Field) | 
| 36 |  | aks6d1c1.14 | . . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ ℙ) | 
| 37 |  | aks6d1c1.15 | . . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ ℕ) | 
| 38 |  | aks6d1c1.16 | . . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 39 |  | aks6d1c1.17 | . . . . . . . 8
⊢ (𝜑 → 𝑃 ∥ 𝑁) | 
| 40 |  | aks6d1c1.18 | . . . . . . . 8
⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) | 
| 41 |  | aks6d1c1.24 | . . . . . . . . . . . 12
⊢ 𝐸 = ((𝑃↑𝑈) · ((𝑁 / 𝑃)↑𝐿)) | 
| 42 |  | prmnn 16712 | . . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) | 
| 43 | 36, 42 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑃 ∈ ℕ) | 
| 44 |  | aks6d1c1.22 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑈 ∈
ℕ0) | 
| 45 | 43, 44 | nnexpcld 14285 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃↑𝑈) ∈ ℕ) | 
| 46 | 43 | nnzd 12642 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑃 ∈ ℤ) | 
| 47 | 43 | nnne0d 12317 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑃 ≠ 0) | 
| 48 | 38 | nnzd 12642 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈ ℤ) | 
| 49 |  | dvdsval2 16294 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ ℤ ∧ 𝑃 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝑃 ∥ 𝑁 ↔ (𝑁 / 𝑃) ∈ ℤ)) | 
| 50 | 46, 47, 48, 49 | syl3anc 1372 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑃 ∥ 𝑁 ↔ (𝑁 / 𝑃) ∈ ℤ)) | 
| 51 | 39, 50 | mpbid 232 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑁 / 𝑃) ∈ ℤ) | 
| 52 | 38 | nnred 12282 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈ ℝ) | 
| 53 | 43 | nnred 12282 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑃 ∈ ℝ) | 
| 54 | 38 | nngt0d 12316 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 0 < 𝑁) | 
| 55 | 43 | nngt0d 12316 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 0 < 𝑃) | 
| 56 | 52, 53, 54, 55 | divgt0d 12204 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 < (𝑁 / 𝑃)) | 
| 57 | 51, 56 | jca 511 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑁 / 𝑃) ∈ ℤ ∧ 0 < (𝑁 / 𝑃))) | 
| 58 |  | elnnz 12625 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 / 𝑃) ∈ ℕ ↔ ((𝑁 / 𝑃) ∈ ℤ ∧ 0 < (𝑁 / 𝑃))) | 
| 59 | 57, 58 | sylibr 234 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑁 / 𝑃) ∈ ℕ) | 
| 60 |  | aks6d1c1.23 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐿 ∈
ℕ0) | 
| 61 | 59, 60 | nnexpcld 14285 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑁 / 𝑃)↑𝐿) ∈ ℕ) | 
| 62 | 45, 61 | nnmulcld 12320 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑃↑𝑈) · ((𝑁 / 𝑃)↑𝐿)) ∈ ℕ) | 
| 63 | 41, 62 | eqeltrid 2844 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈ ℕ) | 
| 64 | 23, 24, 25, 26, 28, 29, 32, 33, 35, 36, 37, 38, 39, 40, 63 | aks6d1c1p7 42115 | . . . . . . . . . 10
⊢ (𝜑 → 𝐸 ∼ 𝑋) | 
| 65 | 35 | fldcrngd 20743 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐾 ∈ CRing) | 
| 66 | 24 | ply1crng 22201 | . . . . . . . . . . . . . 14
⊢ (𝐾 ∈ CRing → 𝑆 ∈ CRing) | 
| 67 | 65, 66 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 ∈ CRing) | 
| 68 |  | crngring 20243 | . . . . . . . . . . . . . 14
⊢ (𝑆 ∈ CRing → 𝑆 ∈ Ring) | 
| 69 |  | ringcmn 20280 | . . . . . . . . . . . . . 14
⊢ (𝑆 ∈ Ring → 𝑆 ∈ CMnd) | 
| 70 | 68, 69 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝑆 ∈ CRing → 𝑆 ∈ CMnd) | 
| 71 | 67, 70 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ∈ CMnd) | 
| 72 |  | cmnmnd 19816 | . . . . . . . . . . . 12
⊢ (𝑆 ∈ CMnd → 𝑆 ∈ Mnd) | 
| 73 | 71, 72 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ Mnd) | 
| 74 |  | crngring 20243 | . . . . . . . . . . . . 13
⊢ (𝐾 ∈ CRing → 𝐾 ∈ Ring) | 
| 75 | 65, 74 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ∈ Ring) | 
| 76 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(Base‘𝑆) =
(Base‘𝑆) | 
| 77 | 26, 24, 76 | vr1cl 22220 | . . . . . . . . . . . 12
⊢ (𝐾 ∈ Ring → 𝑋 ∈ (Base‘𝑆)) | 
| 78 | 75, 77 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ (Base‘𝑆)) | 
| 79 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(0g‘𝑆) = (0g‘𝑆) | 
| 80 | 76, 34, 79 | mndrid 18769 | . . . . . . . . . . 11
⊢ ((𝑆 ∈ Mnd ∧ 𝑋 ∈ (Base‘𝑆)) → (𝑋 + (0g‘𝑆)) = 𝑋) | 
| 81 | 73, 78, 80 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 → (𝑋 + (0g‘𝑆)) = 𝑋) | 
| 82 | 64, 81 | breqtrrd 5170 | . . . . . . . . 9
⊢ (𝜑 → 𝐸 ∼ (𝑋 + (0g‘𝑆))) | 
| 83 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢
(ℤRHom‘𝐾) = (ℤRHom‘𝐾) | 
| 84 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢
(0g‘𝐾) = (0g‘𝐾) | 
| 85 | 83, 84 | zrh0 21525 | . . . . . . . . . . . . 13
⊢ (𝐾 ∈ Ring →
((ℤRHom‘𝐾)‘0) = (0g‘𝐾)) | 
| 86 | 75, 85 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → ((ℤRHom‘𝐾)‘0) =
(0g‘𝐾)) | 
| 87 | 86 | fveq2d 6909 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐶‘((ℤRHom‘𝐾)‘0)) = (𝐶‘(0g‘𝐾))) | 
| 88 | 24, 30, 84, 79, 75 | ply1ascl0 22257 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐶‘(0g‘𝐾)) = (0g‘𝑆)) | 
| 89 | 87, 88 | eqtrd 2776 | . . . . . . . . . 10
⊢ (𝜑 → (𝐶‘((ℤRHom‘𝐾)‘0)) = (0g‘𝑆)) | 
| 90 | 89 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝜑 → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))) = (𝑋 + (0g‘𝑆))) | 
| 91 | 82, 90 | breqtrrd 5170 | . . . . . . . 8
⊢ (𝜑 → 𝐸 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0)))) | 
| 92 |  | aks6d1c1.19 | . . . . . . . . 9
⊢ (𝜑 → 𝐹:(0...𝐴)⟶ℕ0) | 
| 93 |  | 0zd 12627 | . . . . . . . . . 10
⊢ (𝜑 → 0 ∈
ℤ) | 
| 94 |  | 0red 11265 | . . . . . . . . . . 11
⊢ (𝜑 → 0 ∈
ℝ) | 
| 95 | 94 | leidd 11830 | . . . . . . . . . 10
⊢ (𝜑 → 0 ≤ 0) | 
| 96 | 93, 2, 93, 95, 3 | elfzd 13556 | . . . . . . . . 9
⊢ (𝜑 → 0 ∈ (0...𝐴)) | 
| 97 | 92, 96 | ffvelcdmd 7104 | . . . . . . . 8
⊢ (𝜑 → (𝐹‘0) ∈
ℕ0) | 
| 98 | 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 91, 97 | aks6d1c1p6 42116 | . . . . . . 7
⊢ (𝜑 → 𝐸 ∼ ((𝐹‘0)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))))) | 
| 99 | 27 | crngmgp 20239 | . . . . . . . . . 10
⊢ (𝑆 ∈ CRing → 𝑊 ∈ CMnd) | 
| 100 | 67, 99 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝑊 ∈ CMnd) | 
| 101 | 100 | cmnmndd 19823 | . . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ Mnd) | 
| 102 |  | 0z 12626 | . . . . . . . . 9
⊢ 0 ∈
ℤ | 
| 103 | 102 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → 0 ∈
ℤ) | 
| 104 |  | eqid 2736 | . . . . . . . . 9
⊢
(Base‘𝑊) =
(Base‘𝑊) | 
| 105 |  | 0le0 12368 | . . . . . . . . . . . 12
⊢ 0 ≤
0 | 
| 106 | 105 | a1i 11 | . . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ 0) | 
| 107 | 103, 2, 103, 106, 3 | elfzd 13556 | . . . . . . . . . 10
⊢ (𝜑 → 0 ∈ (0...𝐴)) | 
| 108 | 92, 107 | ffvelcdmd 7104 | . . . . . . . . 9
⊢ (𝜑 → (𝐹‘0) ∈
ℕ0) | 
| 109 | 83 | zrhrhm 21523 | . . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ Ring →
(ℤRHom‘𝐾)
∈ (ℤring RingHom 𝐾)) | 
| 110 | 75, 109 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (ℤRHom‘𝐾) ∈ (ℤring
RingHom 𝐾)) | 
| 111 |  | zringbas 21465 | . . . . . . . . . . . . . . 15
⊢ ℤ =
(Base‘ℤring) | 
| 112 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢
(Base‘𝐾) =
(Base‘𝐾) | 
| 113 | 111, 112 | rhmf 20486 | . . . . . . . . . . . . . 14
⊢
((ℤRHom‘𝐾) ∈ (ℤring RingHom
𝐾) →
(ℤRHom‘𝐾):ℤ⟶(Base‘𝐾)) | 
| 114 | 110, 113 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (ℤRHom‘𝐾):ℤ⟶(Base‘𝐾)) | 
| 115 | 114, 93 | ffvelcdmd 7104 | . . . . . . . . . . . 12
⊢ (𝜑 → ((ℤRHom‘𝐾)‘0) ∈
(Base‘𝐾)) | 
| 116 | 24, 30, 112, 76 | ply1sclcl 22290 | . . . . . . . . . . . 12
⊢ ((𝐾 ∈ Ring ∧
((ℤRHom‘𝐾)‘0) ∈ (Base‘𝐾)) → (𝐶‘((ℤRHom‘𝐾)‘0)) ∈ (Base‘𝑆)) | 
| 117 | 75, 115, 116 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐶‘((ℤRHom‘𝐾)‘0)) ∈ (Base‘𝑆)) | 
| 118 | 76, 34 | mndcl 18756 | . . . . . . . . . . 11
⊢ ((𝑆 ∈ Mnd ∧ 𝑋 ∈ (Base‘𝑆) ∧ (𝐶‘((ℤRHom‘𝐾)‘0)) ∈ (Base‘𝑆)) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))) ∈ (Base‘𝑆)) | 
| 119 | 73, 78, 117, 118 | syl3anc 1372 | . . . . . . . . . 10
⊢ (𝜑 → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))) ∈ (Base‘𝑆)) | 
| 120 | 27, 76 | mgpbas 20143 | . . . . . . . . . 10
⊢
(Base‘𝑆) =
(Base‘𝑊) | 
| 121 | 119, 120 | eleqtrdi 2850 | . . . . . . . . 9
⊢ (𝜑 → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))) ∈ (Base‘𝑊)) | 
| 122 | 104, 31, 101, 108, 121 | mulgnn0cld 19114 | . . . . . . . 8
⊢ (𝜑 → ((𝐹‘0)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0)))) ∈ (Base‘𝑊)) | 
| 123 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑖 = 0 → (𝐹‘𝑖) = (𝐹‘0)) | 
| 124 |  | 2fveq3 6910 | . . . . . . . . . . 11
⊢ (𝑖 = 0 → (𝐶‘((ℤRHom‘𝐾)‘𝑖)) = (𝐶‘((ℤRHom‘𝐾)‘0))) | 
| 125 | 124 | oveq2d 7448 | . . . . . . . . . 10
⊢ (𝑖 = 0 → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))) = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0)))) | 
| 126 | 123, 125 | oveq12d 7450 | . . . . . . . . 9
⊢ (𝑖 = 0 → ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))) = ((𝐹‘0)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))))) | 
| 127 | 104, 126 | gsumsn 19973 | . . . . . . . 8
⊢ ((𝑊 ∈ Mnd ∧ 0 ∈
ℤ ∧ ((𝐹‘0)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0)))) ∈ (Base‘𝑊)) → (𝑊 Σg (𝑖 ∈ {0} ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = ((𝐹‘0)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))))) | 
| 128 | 101, 103,
122, 127 | syl3anc 1372 | . . . . . . 7
⊢ (𝜑 → (𝑊 Σg (𝑖 ∈ {0} ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = ((𝐹‘0)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0))))) | 
| 129 | 98, 128 | breqtrrd 5170 | . . . . . 6
⊢ (𝜑 → 𝐸 ∼ (𝑊 Σg (𝑖 ∈ {0} ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) | 
| 130 |  | fzsn 13607 | . . . . . . . . . 10
⊢ (0 ∈
ℤ → (0...0) = {0}) | 
| 131 | 102, 130 | ax-mp 5 | . . . . . . . . 9
⊢ (0...0) =
{0} | 
| 132 | 131 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → (0...0) =
{0}) | 
| 133 | 132 | mpteq1d 5236 | . . . . . . 7
⊢ (𝜑 → (𝑖 ∈ (0...0) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑖 ∈ {0} ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) | 
| 134 | 133 | oveq2d 7448 | . . . . . 6
⊢ (𝜑 → (𝑊 Σg (𝑖 ∈ (0...0) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σg (𝑖 ∈ {0} ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) | 
| 135 | 129, 134 | breqtrrd 5170 | . . . . 5
⊢ (𝜑 → 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...0) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) | 
| 136 | 35 | 3ad2ant1 1133 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐾 ∈ Field) | 
| 137 | 36 | 3ad2ant1 1133 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑃 ∈ ℙ) | 
| 138 | 37 | 3ad2ant1 1133 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑅 ∈ ℕ) | 
| 139 | 40 | 3ad2ant1 1133 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → (𝑁 gcd 𝑅) = 1) | 
| 140 | 39 | 3ad2ant1 1133 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑃 ∥ 𝑁) | 
| 141 |  | simp3 1138 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) | 
| 142 |  | nfcv 2904 | . . . . . . . . . . 11
⊢
Ⅎ𝑘((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))) | 
| 143 |  | nfcv 2904 | . . . . . . . . . . 11
⊢
Ⅎ𝑖((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))) | 
| 144 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑖 = 𝑘 → (𝐹‘𝑖) = (𝐹‘𝑘)) | 
| 145 |  | 2fveq3 6910 | . . . . . . . . . . . . 13
⊢ (𝑖 = 𝑘 → (𝐶‘((ℤRHom‘𝐾)‘𝑖)) = (𝐶‘((ℤRHom‘𝐾)‘𝑘))) | 
| 146 | 145 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ (𝑖 = 𝑘 → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))) = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))) | 
| 147 | 144, 146 | oveq12d 7450 | . . . . . . . . . . 11
⊢ (𝑖 = 𝑘 → ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))) = ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))) | 
| 148 | 142, 143,
147 | cbvmpt 5252 | . . . . . . . . . 10
⊢ (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑘 ∈ (0...𝑗) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))) | 
| 149 | 148 | oveq2i 7443 | . . . . . . . . 9
⊢ (𝑊 Σg
(𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σg (𝑘 ∈ (0...𝑗) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))) | 
| 150 | 149 | a1i 11 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σg (𝑘 ∈ (0...𝑗) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))))) | 
| 151 | 141, 150 | breqtrd 5168 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐸 ∼ (𝑊 Σg (𝑘 ∈ (0...𝑗) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))))) | 
| 152 | 35 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐾 ∈ Field) | 
| 153 | 36 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑃 ∈ ℙ) | 
| 154 | 37 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑅 ∈ ℕ) | 
| 155 | 38 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑁 ∈ ℕ) | 
| 156 | 39 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑃 ∥ 𝑁) | 
| 157 | 40 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑁 gcd 𝑅) = 1) | 
| 158 | 41 | a1i 11 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐸 = ((𝑃↑𝑈) · ((𝑁 / 𝑃)↑𝐿))) | 
| 159 | 37 | nnzd 12642 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑅 ∈ ℤ) | 
| 160 | 51, 159, 60 | 3jca 1128 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑁 / 𝑃) ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝐿 ∈
ℕ0)) | 
| 161 | 159, 51, 48 | 3jca 1128 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑅 ∈ ℤ ∧ (𝑁 / 𝑃) ∈ ℤ ∧ 𝑁 ∈ ℤ)) | 
| 162 | 48, 159 | jca 511 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ)) | 
| 163 |  | gcdcom 16551 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ) → (𝑁 gcd 𝑅) = (𝑅 gcd 𝑁)) | 
| 164 | 162, 163 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑁 gcd 𝑅) = (𝑅 gcd 𝑁)) | 
| 165 |  | eqeq1 2740 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 gcd 𝑅) = (𝑅 gcd 𝑁) → ((𝑁 gcd 𝑅) = 1 ↔ (𝑅 gcd 𝑁) = 1)) | 
| 166 | 164, 165 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑁 gcd 𝑅) = 1 ↔ (𝑅 gcd 𝑁) = 1)) | 
| 167 | 166 | pm5.74i 271 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 → (𝑁 gcd 𝑅) = 1) ↔ (𝜑 → (𝑅 gcd 𝑁) = 1)) | 
| 168 | 40, 167 | mpbi 230 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑅 gcd 𝑁) = 1) | 
| 169 | 52 | recnd 11290 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑁 ∈ ℂ) | 
| 170 | 53 | recnd 11290 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑃 ∈ ℂ) | 
| 171 | 94, 54 | gtned 11397 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑁 ≠ 0) | 
| 172 | 169, 169,
170, 171, 47 | divdiv2d 12076 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑁 / (𝑁 / 𝑃)) = ((𝑁 · 𝑃) / 𝑁)) | 
| 173 | 169, 170 | mulcomd 11283 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑁 · 𝑃) = (𝑃 · 𝑁)) | 
| 174 | 173 | oveq1d 7447 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑁 · 𝑃) / 𝑁) = ((𝑃 · 𝑁) / 𝑁)) | 
| 175 | 170, 169,
169, 171, 171 | divdiv2d 12076 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑃 / (𝑁 / 𝑁)) = ((𝑃 · 𝑁) / 𝑁)) | 
| 176 | 175 | eqcomd 2742 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑃 · 𝑁) / 𝑁) = (𝑃 / (𝑁 / 𝑁))) | 
| 177 | 174, 176 | eqtrd 2776 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑁 · 𝑃) / 𝑁) = (𝑃 / (𝑁 / 𝑁))) | 
| 178 | 169, 171 | dividd 12042 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑁 / 𝑁) = 1) | 
| 179 | 178 | oveq2d 7448 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑃 / (𝑁 / 𝑁)) = (𝑃 / 1)) | 
| 180 | 170 | div1d 12036 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑃 / 1) = 𝑃) | 
| 181 | 179, 180 | eqtrd 2776 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑃 / (𝑁 / 𝑁)) = 𝑃) | 
| 182 | 181, 46 | eqeltrd 2840 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑃 / (𝑁 / 𝑁)) ∈ ℤ) | 
| 183 | 177, 182 | eqeltrd 2840 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑁 · 𝑃) / 𝑁) ∈ ℤ) | 
| 184 | 172, 183 | eqeltrd 2840 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑁 / (𝑁 / 𝑃)) ∈ ℤ) | 
| 185 | 94, 56 | gtned 11397 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑁 / 𝑃) ≠ 0) | 
| 186 |  | dvdsval2 16294 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 / 𝑃) ∈ ℤ ∧ (𝑁 / 𝑃) ≠ 0 ∧ 𝑁 ∈ ℤ) → ((𝑁 / 𝑃) ∥ 𝑁 ↔ (𝑁 / (𝑁 / 𝑃)) ∈ ℤ)) | 
| 187 | 51, 185, 48, 186 | syl3anc 1372 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑁 / 𝑃) ∥ 𝑁 ↔ (𝑁 / (𝑁 / 𝑃)) ∈ ℤ)) | 
| 188 | 184, 187 | mpbird 257 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑁 / 𝑃) ∥ 𝑁) | 
| 189 | 168, 188 | jca 511 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑅 gcd 𝑁) = 1 ∧ (𝑁 / 𝑃) ∥ 𝑁)) | 
| 190 |  | rpdvds 16698 | . . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ ℤ ∧ (𝑁 / 𝑃) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑅 gcd 𝑁) = 1 ∧ (𝑁 / 𝑃) ∥ 𝑁)) → (𝑅 gcd (𝑁 / 𝑃)) = 1) | 
| 191 | 161, 189,
190 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑅 gcd (𝑁 / 𝑃)) = 1) | 
| 192 | 159, 51 | jca 511 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑅 ∈ ℤ ∧ (𝑁 / 𝑃) ∈ ℤ)) | 
| 193 |  | gcdcom 16551 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℤ ∧ (𝑁 / 𝑃) ∈ ℤ) → (𝑅 gcd (𝑁 / 𝑃)) = ((𝑁 / 𝑃) gcd 𝑅)) | 
| 194 | 192, 193 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑅 gcd (𝑁 / 𝑃)) = ((𝑁 / 𝑃) gcd 𝑅)) | 
| 195 |  | eqeq1 2740 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑅 gcd (𝑁 / 𝑃)) = ((𝑁 / 𝑃) gcd 𝑅) → ((𝑅 gcd (𝑁 / 𝑃)) = 1 ↔ ((𝑁 / 𝑃) gcd 𝑅) = 1)) | 
| 196 | 194, 195 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑅 gcd (𝑁 / 𝑃)) = 1 ↔ ((𝑁 / 𝑃) gcd 𝑅) = 1)) | 
| 197 | 196 | pm5.74i 271 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 → (𝑅 gcd (𝑁 / 𝑃)) = 1) ↔ (𝜑 → ((𝑁 / 𝑃) gcd 𝑅) = 1)) | 
| 198 | 191, 197 | mpbi 230 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑁 / 𝑃) gcd 𝑅) = 1) | 
| 199 |  | rpexp1i 16761 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 / 𝑃) ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝐿 ∈ ℕ0) → (((𝑁 / 𝑃) gcd 𝑅) = 1 → (((𝑁 / 𝑃)↑𝐿) gcd 𝑅) = 1)) | 
| 200 | 199 | imp 406 | . . . . . . . . . . . . . 14
⊢ ((((𝑁 / 𝑃) ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝐿 ∈ ℕ0) ∧ ((𝑁 / 𝑃) gcd 𝑅) = 1) → (((𝑁 / 𝑃)↑𝐿) gcd 𝑅) = 1) | 
| 201 | 160, 198,
200 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑁 / 𝑃)↑𝐿) gcd 𝑅) = 1) | 
| 202 | 201 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (((𝑁 / 𝑃)↑𝐿) gcd 𝑅) = 1) | 
| 203 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))) = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))) | 
| 204 |  | simpr1 1194 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑗 ∈ ℤ) | 
| 205 | 204 | peano2zd 12727 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑗 + 1) ∈ ℤ) | 
| 206 | 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 152, 153, 154, 157, 156, 203, 205 | aks6d1c1p2 42111 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑃 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))) | 
| 207 | 44 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑈 ∈
ℕ0) | 
| 208 | 159, 46, 48 | 3jca 1128 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑅 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ)) | 
| 209 | 168, 39 | jca 511 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑅 gcd 𝑁) = 1 ∧ 𝑃 ∥ 𝑁)) | 
| 210 |  | rpdvds 16698 | . . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑅 gcd 𝑁) = 1 ∧ 𝑃 ∥ 𝑁)) → (𝑅 gcd 𝑃) = 1) | 
| 211 | 208, 209,
210 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑅 gcd 𝑃) = 1) | 
| 212 | 159, 46 | jca 511 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑅 ∈ ℤ ∧ 𝑃 ∈ ℤ)) | 
| 213 |  | gcdcom 16551 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝑅 gcd 𝑃) = (𝑃 gcd 𝑅)) | 
| 214 | 212, 213 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑅 gcd 𝑃) = (𝑃 gcd 𝑅)) | 
| 215 |  | eqeq1 2740 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑅 gcd 𝑃) = (𝑃 gcd 𝑅) → ((𝑅 gcd 𝑃) = 1 ↔ (𝑃 gcd 𝑅) = 1)) | 
| 216 | 214, 215 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑅 gcd 𝑃) = 1 ↔ (𝑃 gcd 𝑅) = 1)) | 
| 217 | 216 | pm5.74i 271 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 → (𝑅 gcd 𝑃) = 1) ↔ (𝜑 → (𝑃 gcd 𝑅) = 1)) | 
| 218 | 211, 217 | mpbi 230 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑃 gcd 𝑅) = 1) | 
| 219 | 218 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑃 gcd 𝑅) = 1) | 
| 220 | 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 152, 153, 154, 155, 156, 157, 206, 207, 219 | aks6d1c1p8 42117 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑃↑𝑈) ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))) | 
| 221 |  | 2fveq3 6910 | . . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (𝑗 + 1) → (𝐶‘((ℤRHom‘𝐾)‘𝑎)) = (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))) | 
| 222 | 221 | oveq2d 7448 | . . . . . . . . . . . . . . . 16
⊢ (𝑎 = (𝑗 + 1) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))) = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))) | 
| 223 | 222 | breq2d 5154 | . . . . . . . . . . . . . . 15
⊢ (𝑎 = (𝑗 + 1) → (𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))) ↔ 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))) | 
| 224 |  | aks6d1c1.25 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))) | 
| 225 | 23, 24, 25, 26, 28, 29, 32, 33, 35, 36, 37, 38, 39, 40, 38 | aks6d1c1p7 42115 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝑁 ∼ 𝑋) | 
| 226 | 225, 81 | breqtrrd 5170 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝑁 ∼ (𝑋 + (0g‘𝑆))) | 
| 227 | 226, 90 | breqtrrd 5170 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0)))) | 
| 228 | 227 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑎 = 0) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0)))) | 
| 229 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑎 = 0) → 𝑎 = 0) | 
| 230 | 229 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑎 = 0) → ((ℤRHom‘𝐾)‘𝑎) = ((ℤRHom‘𝐾)‘0)) | 
| 231 | 230 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑎 = 0) → (𝐶‘((ℤRHom‘𝐾)‘𝑎)) = (𝐶‘((ℤRHom‘𝐾)‘0))) | 
| 232 | 231 | oveq2d 7448 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑎 = 0) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))) = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘0)))) | 
| 233 | 228, 232 | breqtrrd 5170 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑎 = 0) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))) | 
| 234 | 233 | ex 412 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑎 = 0 → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) | 
| 235 | 234 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → (𝑎 = 0 → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) | 
| 236 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) | 
| 237 |  | 1cnd 11257 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → 1 ∈
ℂ) | 
| 238 | 237 | addlidd 11463 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → (0 + 1) = 1) | 
| 239 | 238 | oveq1d 7447 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → ((0 + 1)...𝐴) = (1...𝐴)) | 
| 240 | 239 | eleq2d 2826 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → (𝑎 ∈ ((0 + 1)...𝐴) ↔ 𝑎 ∈ (1...𝐴))) | 
| 241 | 240 | imbi1d 341 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → ((𝑎 ∈ ((0 + 1)...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))) ↔ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))))) | 
| 242 | 236, 241 | mpbird 257 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → (𝑎 ∈ ((0 + 1)...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) | 
| 243 | 235, 242 | jaod 859 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → ((𝑎 = 0 ∨ 𝑎 ∈ ((0 + 1)...𝐴)) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) | 
| 244 | 2, 3 | jca 511 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝐴 ∈ ℤ ∧ 0 ≤ 𝐴)) | 
| 245 |  | eluz1 12883 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (0 ∈
ℤ → (𝐴 ∈
(ℤ≥‘0) ↔ (𝐴 ∈ ℤ ∧ 0 ≤ 𝐴))) | 
| 246 | 93, 245 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝐴 ∈ (ℤ≥‘0)
↔ (𝐴 ∈ ℤ
∧ 0 ≤ 𝐴))) | 
| 247 | 244, 246 | mpbird 257 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐴 ∈
(ℤ≥‘0)) | 
| 248 | 247 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → 𝐴 ∈
(ℤ≥‘0)) | 
| 249 |  | elfzp12 13644 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐴 ∈
(ℤ≥‘0) → (𝑎 ∈ (0...𝐴) ↔ (𝑎 = 0 ∨ 𝑎 ∈ ((0 + 1)...𝐴)))) | 
| 250 | 248, 249 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → (𝑎 ∈ (0...𝐴) ↔ (𝑎 = 0 ∨ 𝑎 ∈ ((0 + 1)...𝐴)))) | 
| 251 | 250 | imbi1d 341 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → ((𝑎 ∈ (0...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))) ↔ ((𝑎 = 0 ∨ 𝑎 ∈ ((0 + 1)...𝐴)) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))))) | 
| 252 | 243, 251 | mpbird 257 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) → (𝑎 ∈ (0...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) | 
| 253 | 252 | ex 412 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑎 ∈ (1...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))) → (𝑎 ∈ (0...𝐴) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))))) | 
| 254 | 253 | ralimdv2 3162 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (∀𝑎 ∈ (1...𝐴)𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))) → ∀𝑎 ∈ (0...𝐴)𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎))))) | 
| 255 | 224, 254 | mpd 15 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∀𝑎 ∈ (0...𝐴)𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))) | 
| 256 | 255 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → ∀𝑎 ∈ (0...𝐴)𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑎)))) | 
| 257 |  | 0zd 12627 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 0 ∈ ℤ) | 
| 258 | 2 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐴 ∈ ℤ) | 
| 259 | 204 | zred 12724 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑗 ∈ ℝ) | 
| 260 |  | 1red 11263 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 1 ∈ ℝ) | 
| 261 |  | simpr2 1195 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 0 ≤ 𝑗) | 
| 262 |  | 0le1 11787 | . . . . . . . . . . . . . . . . . 18
⊢ 0 ≤
1 | 
| 263 | 262 | a1i 11 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 0 ≤ 1) | 
| 264 | 259, 260,
261, 263 | addge0d 11840 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 0 ≤ (𝑗 + 1)) | 
| 265 |  | simpr3 1196 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑗 < 𝐴) | 
| 266 | 204, 258 | zltp1led 41981 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑗 < 𝐴 ↔ (𝑗 + 1) ≤ 𝐴)) | 
| 267 | 265, 266 | mpbid 232 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑗 + 1) ≤ 𝐴) | 
| 268 | 257, 258,
205, 264, 267 | elfzd 13556 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑗 + 1) ∈ (0...𝐴)) | 
| 269 | 223, 256,
268 | rspcdva 3622 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑁 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))) | 
| 270 |  | aks6d1c1.26 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃 ↑ 𝑥)) ∈ (𝐾 RingIso 𝐾)) | 
| 271 | 270 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃 ↑ 𝑥)) ∈ (𝐾 RingIso 𝐾)) | 
| 272 | 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 152, 153, 154, 157, 156, 203, 205, 269, 271 | aks6d1c1p3 42112 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑁 / 𝑃) ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))) | 
| 273 | 60 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐿 ∈
ℕ0) | 
| 274 | 198 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → ((𝑁 / 𝑃) gcd 𝑅) = 1) | 
| 275 | 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 152, 153, 154, 155, 156, 157, 272, 273, 274 | aks6d1c1p8 42117 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → ((𝑁 / 𝑃)↑𝐿) ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))) | 
| 276 | 23, 24, 25, 26, 27, 28, 29, 30, 32, 33, 34, 152, 153, 154, 202, 156, 220, 275 | aks6d1c1p5 42114 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → ((𝑃↑𝑈) · ((𝑁 / 𝑃)↑𝐿)) ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))) | 
| 277 | 158, 276 | eqbrtrd 5164 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐸 ∼ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))) | 
| 278 | 92 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐹:(0...𝐴)⟶ℕ0) | 
| 279 | 278, 268 | ffvelcdmd 7104 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝐹‘(𝑗 + 1)) ∈
ℕ0) | 
| 280 | 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 152, 153, 154, 155, 156, 157, 277, 279 | aks6d1c1p6 42116 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐸 ∼ ((𝐹‘(𝑗 + 1))𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))) | 
| 281 | 101 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑊 ∈ Mnd) | 
| 282 |  | ovexd 7467 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑗 + 1) ∈ V) | 
| 283 | 73 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑆 ∈ Mnd) | 
| 284 | 78 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝑋 ∈ (Base‘𝑆)) | 
| 285 | 75 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐾 ∈ Ring) | 
| 286 | 114 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (ℤRHom‘𝐾):ℤ⟶(Base‘𝐾)) | 
| 287 | 286, 205 | ffvelcdmd 7104 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → ((ℤRHom‘𝐾)‘(𝑗 + 1)) ∈ (Base‘𝐾)) | 
| 288 | 24, 30, 112, 76 | ply1sclcl 22290 | . . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ Ring ∧
((ℤRHom‘𝐾)‘(𝑗 + 1)) ∈ (Base‘𝐾)) → (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))) ∈ (Base‘𝑆)) | 
| 289 | 285, 287,
288 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))) ∈ (Base‘𝑆)) | 
| 290 | 76, 34 | mndcl 18756 | . . . . . . . . . . . . 13
⊢ ((𝑆 ∈ Mnd ∧ 𝑋 ∈ (Base‘𝑆) ∧ (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))) ∈ (Base‘𝑆)) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))) ∈ (Base‘𝑆)) | 
| 291 | 283, 284,
289, 290 | syl3anc 1372 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))) ∈ (Base‘𝑆)) | 
| 292 | 291, 120 | eleqtrdi 2850 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))) ∈ (Base‘𝑊)) | 
| 293 | 104, 31, 281, 279, 292 | mulgnn0cld 19114 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → ((𝐹‘(𝑗 + 1))𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))) ∈ (Base‘𝑊)) | 
| 294 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑘 = (𝑗 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑗 + 1))) | 
| 295 |  | 2fveq3 6910 | . . . . . . . . . . . . 13
⊢ (𝑘 = (𝑗 + 1) → (𝐶‘((ℤRHom‘𝐾)‘𝑘)) = (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))) | 
| 296 | 295 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ (𝑘 = (𝑗 + 1) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))) = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))) | 
| 297 | 294, 296 | oveq12d 7450 | . . . . . . . . . . 11
⊢ (𝑘 = (𝑗 + 1) → ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))) = ((𝐹‘(𝑗 + 1))𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))) | 
| 298 | 104, 297 | gsumsn 19973 | . . . . . . . . . 10
⊢ ((𝑊 ∈ Mnd ∧ (𝑗 + 1) ∈ V ∧ ((𝐹‘(𝑗 + 1))𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1))))) ∈ (Base‘𝑊)) → (𝑊 Σg (𝑘 ∈ {(𝑗 + 1)} ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))) = ((𝐹‘(𝑗 + 1))𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))) | 
| 299 | 281, 282,
293, 298 | syl3anc 1372 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → (𝑊 Σg (𝑘 ∈ {(𝑗 + 1)} ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))) = ((𝐹‘(𝑗 + 1))𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘(𝑗 + 1)))))) | 
| 300 | 280, 299 | breqtrrd 5170 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴)) → 𝐸 ∼ (𝑊 Σg (𝑘 ∈ {(𝑗 + 1)} ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))))) | 
| 301 | 300 | 3adant3 1132 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐸 ∼ (𝑊 Σg (𝑘 ∈ {(𝑗 + 1)} ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))))) | 
| 302 | 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 136, 137, 138, 139, 140, 151, 301 | aks6d1c1p4 42113 | . . . . . 6
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐸 ∼ ((𝑊 Σg (𝑘 ∈ (0...𝑗) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))))(+g‘𝑊)(𝑊 Σg (𝑘 ∈ {(𝑗 + 1)} ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))))) | 
| 303 | 142, 143,
147 | cbvmpt 5252 | . . . . . . . . 9
⊢ (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑘 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))) | 
| 304 | 303 | a1i 11 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑘 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))) | 
| 305 | 304 | oveq2d 7448 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → (𝑊 Σg (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σg (𝑘 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))))) | 
| 306 |  | eqid 2736 | . . . . . . . 8
⊢
(+g‘𝑊) = (+g‘𝑊) | 
| 307 | 100 | 3ad2ant1 1133 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑊 ∈ CMnd) | 
| 308 |  | simp21 1206 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑗 ∈ ℤ) | 
| 309 |  | simp22 1207 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 0 ≤ 𝑗) | 
| 310 | 308, 309 | jca 511 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗)) | 
| 311 |  | elnn0z 12628 | . . . . . . . . 9
⊢ (𝑗 ∈ ℕ0
↔ (𝑗 ∈ ℤ
∧ 0 ≤ 𝑗)) | 
| 312 | 310, 311 | sylibr 234 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑗 ∈ ℕ0) | 
| 313 | 281 | 3adant3 1132 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑊 ∈ Mnd) | 
| 314 | 313 | adantr 480 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑊 ∈ Mnd) | 
| 315 | 92 | 3ad2ant1 1133 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐹:(0...𝐴)⟶ℕ0) | 
| 316 | 315 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝐹:(0...𝐴)⟶ℕ0) | 
| 317 |  | 0zd 12627 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 0 ∈
ℤ) | 
| 318 | 2 | 3ad2ant1 1133 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐴 ∈ ℤ) | 
| 319 | 318 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝐴 ∈ ℤ) | 
| 320 |  | elfzelz 13565 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ (0...(𝑗 + 1)) → 𝑘 ∈ ℤ) | 
| 321 | 320 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑘 ∈ ℤ) | 
| 322 |  | elfzle1 13568 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ (0...(𝑗 + 1)) → 0 ≤ 𝑘) | 
| 323 | 322 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 0 ≤ 𝑘) | 
| 324 | 321 | zred 12724 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑘 ∈ ℝ) | 
| 325 | 308 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑗 ∈ ℤ) | 
| 326 | 325 | zred 12724 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑗 ∈ ℝ) | 
| 327 |  | 1red 11263 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 1 ∈
ℝ) | 
| 328 | 326, 327 | readdcld 11291 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (𝑗 + 1) ∈ ℝ) | 
| 329 | 319 | zred 12724 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝐴 ∈ ℝ) | 
| 330 |  | elfzle2 13569 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ (0...(𝑗 + 1)) → 𝑘 ≤ (𝑗 + 1)) | 
| 331 | 330 | adantl 481 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑘 ≤ (𝑗 + 1)) | 
| 332 |  | simpl23 1253 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑗 < 𝐴) | 
| 333 | 325, 319 | zltp1led 41981 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (𝑗 < 𝐴 ↔ (𝑗 + 1) ≤ 𝐴)) | 
| 334 | 332, 333 | mpbid 232 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (𝑗 + 1) ≤ 𝐴) | 
| 335 | 324, 328,
329, 331, 334 | letrd 11419 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑘 ≤ 𝐴) | 
| 336 | 317, 319,
321, 323, 335 | elfzd 13556 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑘 ∈ (0...𝐴)) | 
| 337 | 316, 336 | ffvelcdmd 7104 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (𝐹‘𝑘) ∈
ℕ0) | 
| 338 | 283 | 3adant3 1132 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑆 ∈ Mnd) | 
| 339 | 338 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑆 ∈ Mnd) | 
| 340 | 284 | 3adant3 1132 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝑋 ∈ (Base‘𝑆)) | 
| 341 | 340 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝑋 ∈ (Base‘𝑆)) | 
| 342 | 285 | 3adant3 1132 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐾 ∈ Ring) | 
| 343 | 342 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → 𝐾 ∈ Ring) | 
| 344 | 343, 109,
113 | 3syl 18 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (ℤRHom‘𝐾):ℤ⟶(Base‘𝐾)) | 
| 345 | 344, 321 | ffvelcdmd 7104 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → ((ℤRHom‘𝐾)‘𝑘) ∈ (Base‘𝐾)) | 
| 346 | 24, 30, 112, 76 | ply1sclcl 22290 | . . . . . . . . . . . 12
⊢ ((𝐾 ∈ Ring ∧
((ℤRHom‘𝐾)‘𝑘) ∈ (Base‘𝐾)) → (𝐶‘((ℤRHom‘𝐾)‘𝑘)) ∈ (Base‘𝑆)) | 
| 347 | 343, 345,
346 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (𝐶‘((ℤRHom‘𝐾)‘𝑘)) ∈ (Base‘𝑆)) | 
| 348 | 76, 34 | mndcl 18756 | . . . . . . . . . . 11
⊢ ((𝑆 ∈ Mnd ∧ 𝑋 ∈ (Base‘𝑆) ∧ (𝐶‘((ℤRHom‘𝐾)‘𝑘)) ∈ (Base‘𝑆)) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))) ∈ (Base‘𝑆)) | 
| 349 | 339, 341,
347, 348 | syl3anc 1372 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))) ∈ (Base‘𝑆)) | 
| 350 | 349, 120 | eleqtrdi 2850 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))) ∈ (Base‘𝑊)) | 
| 351 | 104, 31, 314, 337, 350 | mulgnn0cld 19114 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) ∧ 𝑘 ∈ (0...(𝑗 + 1))) → ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))) ∈ (Base‘𝑊)) | 
| 352 | 104, 306,
307, 312, 351 | gsummptfzsplit 19951 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → (𝑊 Σg (𝑘 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))) = ((𝑊 Σg (𝑘 ∈ (0...𝑗) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))))(+g‘𝑊)(𝑊 Σg (𝑘 ∈ {(𝑗 + 1)} ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))))) | 
| 353 | 305, 352 | eqtrd 2776 | . . . . . 6
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → (𝑊 Σg (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = ((𝑊 Σg (𝑘 ∈ (0...𝑗) ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘))))))(+g‘𝑊)(𝑊 Σg (𝑘 ∈ {(𝑗 + 1)} ↦ ((𝐹‘𝑘)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑘)))))))) | 
| 354 | 302, 353 | breqtrrd 5170 | . . . . 5
⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ∧ 𝑗 < 𝐴) ∧ 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝑗) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) → 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...(𝑗 + 1)) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) | 
| 355 | 10, 14, 18, 22, 135, 354, 93, 2, 3 | fzindd 12722 | . . . 4
⊢ ((𝜑 ∧ (𝐴 ∈ ℤ ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐴)) → 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) | 
| 356 | 355 | ex 412 | . . 3
⊢ (𝜑 → ((𝐴 ∈ ℤ ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐴) → 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))) | 
| 357 | 6, 356 | mpd 15 | . 2
⊢ (𝜑 → 𝐸 ∼ (𝑊 Σg (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) | 
| 358 |  | aks6d1c1.20 | . . . 4
⊢ 𝐺 = (𝑔 ∈ (ℕ0
↑m (0...𝐴))
↦ (𝑊
Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) | 
| 359 | 358 | a1i 11 | . . 3
⊢ (𝜑 → 𝐺 = (𝑔 ∈ (ℕ0
↑m (0...𝐴))
↦ (𝑊
Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))))) | 
| 360 |  | simplr 768 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑔 = 𝐹) ∧ 𝑖 ∈ (0...𝐴)) → 𝑔 = 𝐹) | 
| 361 | 360 | fveq1d 6907 | . . . . . 6
⊢ (((𝜑 ∧ 𝑔 = 𝐹) ∧ 𝑖 ∈ (0...𝐴)) → (𝑔‘𝑖) = (𝐹‘𝑖)) | 
| 362 | 361 | oveq1d 7447 | . . . . 5
⊢ (((𝜑 ∧ 𝑔 = 𝐹) ∧ 𝑖 ∈ (0...𝐴)) → ((𝑔‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))) = ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) | 
| 363 | 362 | mpteq2dva 5241 | . . . 4
⊢ ((𝜑 ∧ 𝑔 = 𝐹) → (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))) = (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) | 
| 364 | 363 | oveq2d 7448 | . . 3
⊢ ((𝜑 ∧ 𝑔 = 𝐹) → (𝑊 Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) = (𝑊 Σg (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) | 
| 365 |  | nn0ex 12534 | . . . . . 6
⊢
ℕ0 ∈ V | 
| 366 | 365 | a1i 11 | . . . . 5
⊢ (𝜑 → ℕ0 ∈
V) | 
| 367 |  | ovexd 7467 | . . . . 5
⊢ (𝜑 → (0...𝐴) ∈ V) | 
| 368 | 366, 367 | elmapd 8881 | . . . 4
⊢ (𝜑 → (𝐹 ∈ (ℕ0
↑m (0...𝐴))
↔ 𝐹:(0...𝐴)⟶ℕ0)) | 
| 369 | 92, 368 | mpbird 257 | . . 3
⊢ (𝜑 → 𝐹 ∈ (ℕ0
↑m (0...𝐴))) | 
| 370 |  | ovexd 7467 | . . 3
⊢ (𝜑 → (𝑊 Σg (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖)))))) ∈ V) | 
| 371 | 359, 364,
369, 370 | fvmptd 7022 | . 2
⊢ (𝜑 → (𝐺‘𝐹) = (𝑊 Σg (𝑖 ∈ (0...𝐴) ↦ ((𝐹‘𝑖)𝐷(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝑖))))))) | 
| 372 | 357, 371 | breqtrrd 5170 | 1
⊢ (𝜑 → 𝐸 ∼ (𝐺‘𝐹)) |