Proof of Theorem expgcd
| Step | Hyp | Ref
| Expression |
| 1 | | gcdnncl 16544 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) ∈ ℕ) |
| 2 | 1 | 3adant3 1133 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (𝐴 gcd 𝐵) ∈
ℕ) |
| 3 | | simp3 1139 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ∈
ℕ0) |
| 4 | 2, 3 | nnexpcld 14284 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ ((𝐴 gcd 𝐵)↑𝑁) ∈ ℕ) |
| 5 | 4 | nncnd 12282 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ ((𝐴 gcd 𝐵)↑𝑁) ∈ ℂ) |
| 6 | 5 | mulridd 11278 |
. 2
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (((𝐴 gcd 𝐵)↑𝑁) · 1) = ((𝐴 gcd 𝐵)↑𝑁)) |
| 7 | | nnexpcl 14115 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (𝐴↑𝑁) ∈
ℕ) |
| 8 | 7 | 3adant2 1132 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (𝐴↑𝑁) ∈
ℕ) |
| 9 | 8 | nnzd 12640 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (𝐴↑𝑁) ∈
ℤ) |
| 10 | | nnexpcl 14115 |
. . . . . . 7
⊢ ((𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (𝐵↑𝑁) ∈
ℕ) |
| 11 | 10 | 3adant1 1131 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (𝐵↑𝑁) ∈
ℕ) |
| 12 | 11 | nnzd 12640 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (𝐵↑𝑁) ∈
ℤ) |
| 13 | | simpl 482 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝐴 ∈
ℕ) |
| 14 | 13 | nnzd 12640 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝐴 ∈
ℤ) |
| 15 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝐵 ∈
ℕ) |
| 16 | 15 | nnzd 12640 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝐵 ∈
ℤ) |
| 17 | | gcddvds 16540 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵)) |
| 18 | 14, 16, 17 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵)) |
| 19 | 18 | 3adant3 1133 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵)) |
| 20 | 19 | simpld 494 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (𝐴 gcd 𝐵) ∥ 𝐴) |
| 21 | 2 | nnzd 12640 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (𝐴 gcd 𝐵) ∈
ℤ) |
| 22 | | simp1 1137 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ 𝐴 ∈
ℕ) |
| 23 | 22 | nnzd 12640 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ 𝐴 ∈
ℤ) |
| 24 | | dvdsexpim 16592 |
. . . . . . 7
⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → ((𝐴 gcd 𝐵) ∥ 𝐴 → ((𝐴 gcd 𝐵)↑𝑁) ∥ (𝐴↑𝑁))) |
| 25 | 21, 23, 3, 24 | syl3anc 1373 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ ((𝐴 gcd 𝐵) ∥ 𝐴 → ((𝐴 gcd 𝐵)↑𝑁) ∥ (𝐴↑𝑁))) |
| 26 | 20, 25 | mpd 15 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ ((𝐴 gcd 𝐵)↑𝑁) ∥ (𝐴↑𝑁)) |
| 27 | 19 | simprd 495 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (𝐴 gcd 𝐵) ∥ 𝐵) |
| 28 | | simp2 1138 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ 𝐵 ∈
ℕ) |
| 29 | 28 | nnzd 12640 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ 𝐵 ∈
ℤ) |
| 30 | | dvdsexpim 16592 |
. . . . . . 7
⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → ((𝐴 gcd 𝐵) ∥ 𝐵 → ((𝐴 gcd 𝐵)↑𝑁) ∥ (𝐵↑𝑁))) |
| 31 | 21, 29, 3, 30 | syl3anc 1373 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ ((𝐴 gcd 𝐵) ∥ 𝐵 → ((𝐴 gcd 𝐵)↑𝑁) ∥ (𝐵↑𝑁))) |
| 32 | 27, 31 | mpd 15 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ ((𝐴 gcd 𝐵)↑𝑁) ∥ (𝐵↑𝑁)) |
| 33 | | gcddiv 16588 |
. . . . 5
⊢ ((((𝐴↑𝑁) ∈ ℤ ∧ (𝐵↑𝑁) ∈ ℤ ∧ ((𝐴 gcd 𝐵)↑𝑁) ∈ ℕ) ∧ (((𝐴 gcd 𝐵)↑𝑁) ∥ (𝐴↑𝑁) ∧ ((𝐴 gcd 𝐵)↑𝑁) ∥ (𝐵↑𝑁))) → (((𝐴↑𝑁) gcd (𝐵↑𝑁)) / ((𝐴 gcd 𝐵)↑𝑁)) = (((𝐴↑𝑁) / ((𝐴 gcd 𝐵)↑𝑁)) gcd ((𝐵↑𝑁) / ((𝐴 gcd 𝐵)↑𝑁)))) |
| 34 | 9, 12, 4, 26, 32, 33 | syl32anc 1380 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (((𝐴↑𝑁) gcd (𝐵↑𝑁)) / ((𝐴 gcd 𝐵)↑𝑁)) = (((𝐴↑𝑁) / ((𝐴 gcd 𝐵)↑𝑁)) gcd ((𝐵↑𝑁) / ((𝐴 gcd 𝐵)↑𝑁)))) |
| 35 | | nncn 12274 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℂ) |
| 36 | 35 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ 𝐴 ∈
ℂ) |
| 37 | 2 | nncnd 12282 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (𝐴 gcd 𝐵) ∈
ℂ) |
| 38 | 2 | nnne0d 12316 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (𝐴 gcd 𝐵) ≠ 0) |
| 39 | 36, 37, 38, 3 | expdivd 14200 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ ((𝐴 / (𝐴 gcd 𝐵))↑𝑁) = ((𝐴↑𝑁) / ((𝐴 gcd 𝐵)↑𝑁))) |
| 40 | | nncn 12274 |
. . . . . . 7
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℂ) |
| 41 | 40 | 3ad2ant2 1135 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ 𝐵 ∈
ℂ) |
| 42 | 41, 37, 38, 3 | expdivd 14200 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ ((𝐵 / (𝐴 gcd 𝐵))↑𝑁) = ((𝐵↑𝑁) / ((𝐴 gcd 𝐵)↑𝑁))) |
| 43 | 39, 42 | oveq12d 7449 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (((𝐴 / (𝐴 gcd 𝐵))↑𝑁) gcd ((𝐵 / (𝐴 gcd 𝐵))↑𝑁)) = (((𝐴↑𝑁) / ((𝐴 gcd 𝐵)↑𝑁)) gcd ((𝐵↑𝑁) / ((𝐴 gcd 𝐵)↑𝑁)))) |
| 44 | | gcddiv 16588 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ (𝐴 gcd 𝐵) ∈ ℕ) ∧ ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵)) → ((𝐴 gcd 𝐵) / (𝐴 gcd 𝐵)) = ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵)))) |
| 45 | 23, 29, 2, 19, 44 | syl31anc 1375 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ ((𝐴 gcd 𝐵) / (𝐴 gcd 𝐵)) = ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵)))) |
| 46 | 37, 38 | dividd 12041 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ ((𝐴 gcd 𝐵) / (𝐴 gcd 𝐵)) = 1) |
| 47 | 45, 46 | eqtr3d 2779 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1) |
| 48 | | divgcdnn 16552 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ) → (𝐴 / (𝐴 gcd 𝐵)) ∈ ℕ) |
| 49 | 22, 29, 48 | syl2anc 584 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (𝐴 / (𝐴 gcd 𝐵)) ∈ ℕ) |
| 50 | 49 | nnnn0d 12587 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (𝐴 / (𝐴 gcd 𝐵)) ∈
ℕ0) |
| 51 | | divgcdnnr 16553 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℕ ∧ 𝐴 ∈ ℤ) → (𝐵 / (𝐴 gcd 𝐵)) ∈ ℕ) |
| 52 | 28, 23, 51 | syl2anc 584 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (𝐵 / (𝐴 gcd 𝐵)) ∈ ℕ) |
| 53 | 52 | nnnn0d 12587 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (𝐵 / (𝐴 gcd 𝐵)) ∈
ℕ0) |
| 54 | | nn0rppwr 16598 |
. . . . . 6
⊢ (((𝐴 / (𝐴 gcd 𝐵)) ∈ ℕ0 ∧ (𝐵 / (𝐴 gcd 𝐵)) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1 → (((𝐴 / (𝐴 gcd 𝐵))↑𝑁) gcd ((𝐵 / (𝐴 gcd 𝐵))↑𝑁)) = 1)) |
| 55 | 50, 53, 3, 54 | syl3anc 1373 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1 → (((𝐴 / (𝐴 gcd 𝐵))↑𝑁) gcd ((𝐵 / (𝐴 gcd 𝐵))↑𝑁)) = 1)) |
| 56 | 47, 55 | mpd 15 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (((𝐴 / (𝐴 gcd 𝐵))↑𝑁) gcd ((𝐵 / (𝐴 gcd 𝐵))↑𝑁)) = 1) |
| 57 | 34, 43, 56 | 3eqtr2d 2783 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (((𝐴↑𝑁) gcd (𝐵↑𝑁)) / ((𝐴 gcd 𝐵)↑𝑁)) = 1) |
| 58 | | gcdnncl 16544 |
. . . . . 6
⊢ (((𝐴↑𝑁) ∈ ℕ ∧ (𝐵↑𝑁) ∈ ℕ) → ((𝐴↑𝑁) gcd (𝐵↑𝑁)) ∈ ℕ) |
| 59 | 58 | nncnd 12282 |
. . . . 5
⊢ (((𝐴↑𝑁) ∈ ℕ ∧ (𝐵↑𝑁) ∈ ℕ) → ((𝐴↑𝑁) gcd (𝐵↑𝑁)) ∈ ℂ) |
| 60 | 8, 11, 59 | syl2anc 584 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ ((𝐴↑𝑁) gcd (𝐵↑𝑁)) ∈ ℂ) |
| 61 | 4 | nnne0d 12316 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ ((𝐴 gcd 𝐵)↑𝑁) ≠ 0) |
| 62 | | ax-1cn 11213 |
. . . . 5
⊢ 1 ∈
ℂ |
| 63 | | divmul 11925 |
. . . . 5
⊢ ((((𝐴↑𝑁) gcd (𝐵↑𝑁)) ∈ ℂ ∧ 1 ∈ ℂ
∧ (((𝐴 gcd 𝐵)↑𝑁) ∈ ℂ ∧ ((𝐴 gcd 𝐵)↑𝑁) ≠ 0)) → ((((𝐴↑𝑁) gcd (𝐵↑𝑁)) / ((𝐴 gcd 𝐵)↑𝑁)) = 1 ↔ (((𝐴 gcd 𝐵)↑𝑁) · 1) = ((𝐴↑𝑁) gcd (𝐵↑𝑁)))) |
| 64 | 62, 63 | mp3an2 1451 |
. . . 4
⊢ ((((𝐴↑𝑁) gcd (𝐵↑𝑁)) ∈ ℂ ∧ (((𝐴 gcd 𝐵)↑𝑁) ∈ ℂ ∧ ((𝐴 gcd 𝐵)↑𝑁) ≠ 0)) → ((((𝐴↑𝑁) gcd (𝐵↑𝑁)) / ((𝐴 gcd 𝐵)↑𝑁)) = 1 ↔ (((𝐴 gcd 𝐵)↑𝑁) · 1) = ((𝐴↑𝑁) gcd (𝐵↑𝑁)))) |
| 65 | 60, 5, 61, 64 | syl12anc 837 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ ((((𝐴↑𝑁) gcd (𝐵↑𝑁)) / ((𝐴 gcd 𝐵)↑𝑁)) = 1 ↔ (((𝐴 gcd 𝐵)↑𝑁) · 1) = ((𝐴↑𝑁) gcd (𝐵↑𝑁)))) |
| 66 | 57, 65 | mpbid 232 |
. 2
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (((𝐴 gcd 𝐵)↑𝑁) · 1) = ((𝐴↑𝑁) gcd (𝐵↑𝑁))) |
| 67 | 6, 66 | eqtr3d 2779 |
1
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ ((𝐴 gcd 𝐵)↑𝑁) = ((𝐴↑𝑁) gcd (𝐵↑𝑁))) |