Proof of Theorem expdioph
| Step | Hyp | Ref
| Expression |
| 1 | | pm4.42 1054 |
. . . 4
⊢ ((𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)) ↔ (((𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)) ∧ ¬ (𝑎‘2) ∈ ℕ))) |
| 2 | | ancom 460 |
. . . . . 6
⊢ (((𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)) ∧ (𝑎‘2) ∈ ℕ) ↔ ((𝑎‘2) ∈ ℕ ∧
(𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))) |
| 3 | | elmapi 8889 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → 𝑎:(1...3)⟶ℕ0) |
| 4 | | df-2 12329 |
. . . . . . . . . . . . . . 15
⊢ 2 = (1 +
1) |
| 5 | | df-3 12330 |
. . . . . . . . . . . . . . . 16
⊢ 3 = (2 +
1) |
| 6 | | ssid 4006 |
. . . . . . . . . . . . . . . 16
⊢ (1...3)
⊆ (1...3) |
| 7 | 5, 6 | jm2.27dlem5 43025 |
. . . . . . . . . . . . . . 15
⊢ (1...2)
⊆ (1...3) |
| 8 | 4, 7 | jm2.27dlem5 43025 |
. . . . . . . . . . . . . 14
⊢ (1...1)
⊆ (1...3) |
| 9 | | 1nn 12277 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℕ |
| 10 | 9 | jm2.27dlem3 43023 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
(1...1) |
| 11 | 8, 10 | sselii 3980 |
. . . . . . . . . . . . 13
⊢ 1 ∈
(1...3) |
| 12 | | ffvelcdm 7101 |
. . . . . . . . . . . . 13
⊢ ((𝑎:(1...3)⟶ℕ0 ∧ 1
∈ (1...3)) → (𝑎‘1) ∈
ℕ0) |
| 13 | 3, 11, 12 | sylancl 586 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → (𝑎‘1) ∈
ℕ0) |
| 14 | 13 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘2) ∈ ℕ) → (𝑎‘1) ∈
ℕ0) |
| 15 | | elnn0 12528 |
. . . . . . . . . . 11
⊢ ((𝑎‘1) ∈
ℕ0 ↔ ((𝑎‘1) ∈ ℕ ∨ (𝑎‘1) = 0)) |
| 16 | 14, 15 | sylib 218 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) ∈ ℕ ∨
(𝑎‘1) =
0)) |
| 17 | | elnn1uz2 12967 |
. . . . . . . . . . . 12
⊢ ((𝑎‘1) ∈ ℕ ↔
((𝑎‘1) = 1 ∨
(𝑎‘1) ∈
(ℤ≥‘2))) |
| 18 | 17 | biimpi 216 |
. . . . . . . . . . 11
⊢ ((𝑎‘1) ∈ ℕ →
((𝑎‘1) = 1 ∨
(𝑎‘1) ∈
(ℤ≥‘2))) |
| 19 | 18 | orim1i 910 |
. . . . . . . . . 10
⊢ (((𝑎‘1) ∈ ℕ ∨
(𝑎‘1) = 0) →
(((𝑎‘1) = 1 ∨
(𝑎‘1) ∈
(ℤ≥‘2)) ∨ (𝑎‘1) = 0)) |
| 20 | 16, 19 | syl 17 |
. . . . . . . . 9
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘2) ∈ ℕ) → (((𝑎‘1) = 1 ∨ (𝑎‘1) ∈
(ℤ≥‘2)) ∨ (𝑎‘1) = 0)) |
| 21 | 20 | biantrurd 532 |
. . . . . . . 8
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)) ↔ ((((𝑎‘1) = 1 ∨ (𝑎‘1) ∈
(ℤ≥‘2)) ∨ (𝑎‘1) = 0) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))))) |
| 22 | | andir 1011 |
. . . . . . . . . 10
⊢
(((((𝑎‘1) = 1
∨ (𝑎‘1) ∈
(ℤ≥‘2)) ∨ (𝑎‘1) = 0) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))) ↔ ((((𝑎‘1) = 1 ∨ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))) ∨ ((𝑎‘1) = 0 ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))))) |
| 23 | | andir 1011 |
. . . . . . . . . . 11
⊢ ((((𝑎‘1) = 1 ∨ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))) ↔ (((𝑎‘1) = 1 ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))) ∨ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))))) |
| 24 | 23 | orbi1i 914 |
. . . . . . . . . 10
⊢
(((((𝑎‘1) = 1
∨ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))) ∨ ((𝑎‘1) = 0 ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))) ↔ ((((𝑎‘1) = 1 ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))) ∨ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))) ∨ ((𝑎‘1) = 0 ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))))) |
| 25 | 22, 24 | bitri 275 |
. . . . . . . . 9
⊢
(((((𝑎‘1) = 1
∨ (𝑎‘1) ∈
(ℤ≥‘2)) ∨ (𝑎‘1) = 0) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))) ↔ ((((𝑎‘1) = 1 ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))) ∨ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))) ∨ ((𝑎‘1) = 0 ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))))) |
| 26 | | nnz 12634 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎‘2) ∈ ℕ →
(𝑎‘2) ∈
ℤ) |
| 27 | | 1exp 14132 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎‘2) ∈ ℤ →
(1↑(𝑎‘2)) =
1) |
| 28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎‘2) ∈ ℕ →
(1↑(𝑎‘2)) =
1) |
| 29 | 28 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘2) ∈ ℕ) →
(1↑(𝑎‘2)) =
1) |
| 30 | 29 | eqeq2d 2748 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘3) = (1↑(𝑎‘2)) ↔ (𝑎‘3) = 1)) |
| 31 | | oveq1 7438 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎‘1) = 1 → ((𝑎‘1)↑(𝑎‘2)) = (1↑(𝑎‘2))) |
| 32 | 31 | eqeq2d 2748 |
. . . . . . . . . . . . . 14
⊢ ((𝑎‘1) = 1 → ((𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)) ↔ (𝑎‘3) = (1↑(𝑎‘2)))) |
| 33 | 32 | bibi1d 343 |
. . . . . . . . . . . . 13
⊢ ((𝑎‘1) = 1 → (((𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)) ↔ (𝑎‘3) = 1) ↔ ((𝑎‘3) = (1↑(𝑎‘2)) ↔ (𝑎‘3) = 1))) |
| 34 | 30, 33 | syl5ibrcom 247 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) = 1 → ((𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)) ↔ (𝑎‘3) = 1))) |
| 35 | 34 | pm5.32d 577 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘2) ∈ ℕ) → (((𝑎‘1) = 1 ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))) ↔ ((𝑎‘1) = 1 ∧ (𝑎‘3) = 1))) |
| 36 | | iba 527 |
. . . . . . . . . . . . 13
⊢ ((𝑎‘2) ∈ ℕ →
((𝑎‘1) ∈
(ℤ≥‘2) ↔ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ))) |
| 37 | 36 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) ∈
(ℤ≥‘2) ↔ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ))) |
| 38 | 37 | anbi1d 631 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘2) ∈ ℕ) → (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))) ↔ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))))) |
| 39 | 35, 38 | orbi12d 919 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘2) ∈ ℕ) → ((((𝑎‘1) = 1 ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))) ∨ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))) ↔ (((𝑎‘1) = 1 ∧ (𝑎‘3) = 1) ∨ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))))) |
| 40 | | 0exp 14138 |
. . . . . . . . . . . . . 14
⊢ ((𝑎‘2) ∈ ℕ →
(0↑(𝑎‘2)) =
0) |
| 41 | 40 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘2) ∈ ℕ) →
(0↑(𝑎‘2)) =
0) |
| 42 | 41 | eqeq2d 2748 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘3) = (0↑(𝑎‘2)) ↔ (𝑎‘3) = 0)) |
| 43 | | oveq1 7438 |
. . . . . . . . . . . . . 14
⊢ ((𝑎‘1) = 0 → ((𝑎‘1)↑(𝑎‘2)) = (0↑(𝑎‘2))) |
| 44 | 43 | eqeq2d 2748 |
. . . . . . . . . . . . 13
⊢ ((𝑎‘1) = 0 → ((𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)) ↔ (𝑎‘3) = (0↑(𝑎‘2)))) |
| 45 | 44 | bibi1d 343 |
. . . . . . . . . . . 12
⊢ ((𝑎‘1) = 0 → (((𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)) ↔ (𝑎‘3) = 0) ↔ ((𝑎‘3) = (0↑(𝑎‘2)) ↔ (𝑎‘3) = 0))) |
| 46 | 42, 45 | syl5ibrcom 247 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) = 0 → ((𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)) ↔ (𝑎‘3) = 0))) |
| 47 | 46 | pm5.32d 577 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘2) ∈ ℕ) → (((𝑎‘1) = 0 ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))) ↔ ((𝑎‘1) = 0 ∧ (𝑎‘3) = 0))) |
| 48 | 39, 47 | orbi12d 919 |
. . . . . . . . 9
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘2) ∈ ℕ) → (((((𝑎‘1) = 1 ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))) ∨ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))) ∨ ((𝑎‘1) = 0 ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))) ↔ ((((𝑎‘1) = 1 ∧ (𝑎‘3) = 1) ∨ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))) ∨ ((𝑎‘1) = 0 ∧ (𝑎‘3) = 0)))) |
| 49 | 25, 48 | bitrid 283 |
. . . . . . . 8
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘2) ∈ ℕ) → (((((𝑎‘1) = 1 ∨ (𝑎‘1) ∈
(ℤ≥‘2)) ∨ (𝑎‘1) = 0) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))) ↔ ((((𝑎‘1) = 1 ∧ (𝑎‘3) = 1) ∨ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))) ∨ ((𝑎‘1) = 0 ∧ (𝑎‘3) = 0)))) |
| 50 | 21, 49 | bitrd 279 |
. . . . . . 7
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)) ↔ ((((𝑎‘1) = 1 ∧ (𝑎‘3) = 1) ∨ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))) ∨ ((𝑎‘1) = 0 ∧ (𝑎‘3) = 0)))) |
| 51 | 50 | pm5.32da 579 |
. . . . . 6
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → (((𝑎‘2) ∈ ℕ ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))) ↔ ((𝑎‘2) ∈ ℕ ∧ ((((𝑎‘1) = 1 ∧ (𝑎‘3) = 1) ∨ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))) ∨ ((𝑎‘1) = 0 ∧ (𝑎‘3) = 0))))) |
| 52 | 2, 51 | bitrid 283 |
. . . . 5
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → (((𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)) ∧ (𝑎‘2) ∈ ℕ) ↔ ((𝑎‘2) ∈ ℕ ∧
((((𝑎‘1) = 1 ∧
(𝑎‘3) = 1) ∨
(((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))) ∨ ((𝑎‘1) = 0 ∧ (𝑎‘3) = 0))))) |
| 53 | | ancom 460 |
. . . . . 6
⊢ (((𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)) ∧ ¬ (𝑎‘2) ∈ ℕ) ↔ (¬
(𝑎‘2) ∈ ℕ
∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))) |
| 54 | | 2nn 12339 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℕ |
| 55 | 54 | jm2.27dlem3 43023 |
. . . . . . . . . . 11
⊢ 2 ∈
(1...2) |
| 56 | 7, 55 | sselii 3980 |
. . . . . . . . . 10
⊢ 2 ∈
(1...3) |
| 57 | | ffvelcdm 7101 |
. . . . . . . . . 10
⊢ ((𝑎:(1...3)⟶ℕ0 ∧ 2
∈ (1...3)) → (𝑎‘2) ∈
ℕ0) |
| 58 | 3, 56, 57 | sylancl 586 |
. . . . . . . . 9
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → (𝑎‘2) ∈
ℕ0) |
| 59 | | elnn0 12528 |
. . . . . . . . . . 11
⊢ ((𝑎‘2) ∈
ℕ0 ↔ ((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0)) |
| 60 | | pm2.53 852 |
. . . . . . . . . . 11
⊢ (((𝑎‘2) ∈ ℕ ∨
(𝑎‘2) = 0) →
(¬ (𝑎‘2) ∈
ℕ → (𝑎‘2)
= 0)) |
| 61 | 59, 60 | sylbi 217 |
. . . . . . . . . 10
⊢ ((𝑎‘2) ∈
ℕ0 → (¬ (𝑎‘2) ∈ ℕ → (𝑎‘2) = 0)) |
| 62 | | 0nnn 12302 |
. . . . . . . . . . 11
⊢ ¬ 0
∈ ℕ |
| 63 | | eleq1 2829 |
. . . . . . . . . . 11
⊢ ((𝑎‘2) = 0 → ((𝑎‘2) ∈ ℕ ↔
0 ∈ ℕ)) |
| 64 | 62, 63 | mtbiri 327 |
. . . . . . . . . 10
⊢ ((𝑎‘2) = 0 → ¬
(𝑎‘2) ∈
ℕ) |
| 65 | 61, 64 | impbid1 225 |
. . . . . . . . 9
⊢ ((𝑎‘2) ∈
ℕ0 → (¬ (𝑎‘2) ∈ ℕ ↔ (𝑎‘2) = 0)) |
| 66 | 58, 65 | syl 17 |
. . . . . . . 8
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → (¬ (𝑎‘2) ∈ ℕ ↔ (𝑎‘2) = 0)) |
| 67 | 66 | anbi1d 631 |
. . . . . . 7
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → ((¬ (𝑎‘2) ∈ ℕ ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))) ↔ ((𝑎‘2) = 0 ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))))) |
| 68 | 13 | nn0cnd 12589 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → (𝑎‘1) ∈ ℂ) |
| 69 | 68 | exp0d 14180 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → ((𝑎‘1)↑0) = 1) |
| 70 | 69 | eqeq2d 2748 |
. . . . . . . . 9
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → ((𝑎‘3) = ((𝑎‘1)↑0) ↔ (𝑎‘3) = 1)) |
| 71 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ ((𝑎‘2) = 0 → ((𝑎‘1)↑(𝑎‘2)) = ((𝑎‘1)↑0)) |
| 72 | 71 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ ((𝑎‘2) = 0 → ((𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)) ↔ (𝑎‘3) = ((𝑎‘1)↑0))) |
| 73 | 72 | bibi1d 343 |
. . . . . . . . 9
⊢ ((𝑎‘2) = 0 → (((𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)) ↔ (𝑎‘3) = 1) ↔ ((𝑎‘3) = ((𝑎‘1)↑0) ↔ (𝑎‘3) = 1))) |
| 74 | 70, 73 | syl5ibrcom 247 |
. . . . . . . 8
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → ((𝑎‘2) = 0 → ((𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)) ↔ (𝑎‘3) = 1))) |
| 75 | 74 | pm5.32d 577 |
. . . . . . 7
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → (((𝑎‘2) = 0 ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))) ↔ ((𝑎‘2) = 0 ∧ (𝑎‘3) = 1))) |
| 76 | 67, 75 | bitrd 279 |
. . . . . 6
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → ((¬ (𝑎‘2) ∈ ℕ ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))) ↔ ((𝑎‘2) = 0 ∧ (𝑎‘3) = 1))) |
| 77 | 53, 76 | bitrid 283 |
. . . . 5
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → (((𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)) ∧ ¬ (𝑎‘2) ∈ ℕ) ↔ ((𝑎‘2) = 0 ∧ (𝑎‘3) =
1))) |
| 78 | 52, 77 | orbi12d 919 |
. . . 4
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → ((((𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)) ∧ ¬ (𝑎‘2) ∈ ℕ)) ↔ (((𝑎‘2) ∈ ℕ ∧
((((𝑎‘1) = 1 ∧
(𝑎‘3) = 1) ∨
(((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))) ∨ ((𝑎‘1) = 0 ∧ (𝑎‘3) = 0))) ∨ ((𝑎‘2) = 0 ∧ (𝑎‘3) = 1)))) |
| 79 | 1, 78 | bitrid 283 |
. . 3
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → ((𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)) ↔ (((𝑎‘2) ∈ ℕ ∧ ((((𝑎‘1) = 1 ∧ (𝑎‘3) = 1) ∨ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))) ∨ ((𝑎‘1) = 0 ∧ (𝑎‘3) = 0))) ∨ ((𝑎‘2) = 0 ∧ (𝑎‘3) = 1)))) |
| 80 | 79 | rabbiia 3440 |
. 2
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))} = {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (((𝑎‘2) ∈ ℕ ∧ ((((𝑎‘1) = 1 ∧ (𝑎‘3) = 1) ∨ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))) ∨ ((𝑎‘1) = 0 ∧ (𝑎‘3) = 0))) ∨ ((𝑎‘2) = 0 ∧ (𝑎‘3) = 1))} |
| 81 | | 3nn0 12544 |
. . . . 5
⊢ 3 ∈
ℕ0 |
| 82 | | ovex 7464 |
. . . . . 6
⊢ (1...3)
∈ V |
| 83 | | mzpproj 42748 |
. . . . . 6
⊢ (((1...3)
∈ V ∧ 2 ∈ (1...3)) → (𝑎 ∈ (ℤ ↑m (1...3))
↦ (𝑎‘2)) ∈
(mzPoly‘(1...3))) |
| 84 | 82, 56, 83 | mp2an 692 |
. . . . 5
⊢ (𝑎 ∈ (ℤ
↑m (1...3)) ↦ (𝑎‘2)) ∈
(mzPoly‘(1...3)) |
| 85 | | elnnrabdioph 42818 |
. . . . 5
⊢ ((3
∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑m (1...3))
↦ (𝑎‘2)) ∈
(mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (𝑎‘2) ∈ ℕ} ∈
(Dioph‘3)) |
| 86 | 81, 84, 85 | mp2an 692 |
. . . 4
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (𝑎‘2) ∈ ℕ} ∈
(Dioph‘3) |
| 87 | | mzpproj 42748 |
. . . . . . . . 9
⊢ (((1...3)
∈ V ∧ 1 ∈ (1...3)) → (𝑎 ∈ (ℤ ↑m (1...3))
↦ (𝑎‘1)) ∈
(mzPoly‘(1...3))) |
| 88 | 82, 11, 87 | mp2an 692 |
. . . . . . . 8
⊢ (𝑎 ∈ (ℤ
↑m (1...3)) ↦ (𝑎‘1)) ∈
(mzPoly‘(1...3)) |
| 89 | | 1z 12647 |
. . . . . . . . 9
⊢ 1 ∈
ℤ |
| 90 | | mzpconstmpt 42751 |
. . . . . . . . 9
⊢ (((1...3)
∈ V ∧ 1 ∈ ℤ) → (𝑎 ∈ (ℤ ↑m (1...3))
↦ 1) ∈ (mzPoly‘(1...3))) |
| 91 | 82, 89, 90 | mp2an 692 |
. . . . . . . 8
⊢ (𝑎 ∈ (ℤ
↑m (1...3)) ↦ 1) ∈
(mzPoly‘(1...3)) |
| 92 | | eqrabdioph 42788 |
. . . . . . . 8
⊢ ((3
∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑m (1...3))
↦ (𝑎‘1)) ∈
(mzPoly‘(1...3)) ∧ (𝑎 ∈ (ℤ ↑m (1...3))
↦ 1) ∈ (mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (𝑎‘1) = 1} ∈
(Dioph‘3)) |
| 93 | 81, 88, 91, 92 | mp3an 1463 |
. . . . . . 7
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (𝑎‘1) = 1} ∈
(Dioph‘3) |
| 94 | | 3nn 12345 |
. . . . . . . . . 10
⊢ 3 ∈
ℕ |
| 95 | 94 | jm2.27dlem3 43023 |
. . . . . . . . 9
⊢ 3 ∈
(1...3) |
| 96 | | mzpproj 42748 |
. . . . . . . . 9
⊢ (((1...3)
∈ V ∧ 3 ∈ (1...3)) → (𝑎 ∈ (ℤ ↑m (1...3))
↦ (𝑎‘3)) ∈
(mzPoly‘(1...3))) |
| 97 | 82, 95, 96 | mp2an 692 |
. . . . . . . 8
⊢ (𝑎 ∈ (ℤ
↑m (1...3)) ↦ (𝑎‘3)) ∈
(mzPoly‘(1...3)) |
| 98 | | eqrabdioph 42788 |
. . . . . . . 8
⊢ ((3
∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑m (1...3))
↦ (𝑎‘3)) ∈
(mzPoly‘(1...3)) ∧ (𝑎 ∈ (ℤ ↑m (1...3))
↦ 1) ∈ (mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (𝑎‘3) = 1} ∈
(Dioph‘3)) |
| 99 | 81, 97, 91, 98 | mp3an 1463 |
. . . . . . 7
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (𝑎‘3) = 1} ∈
(Dioph‘3) |
| 100 | | anrabdioph 42791 |
. . . . . . 7
⊢ (({𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (𝑎‘1) = 1} ∈ (Dioph‘3) ∧
{𝑎 ∈
(ℕ0 ↑m (1...3)) ∣ (𝑎‘3) = 1} ∈ (Dioph‘3)) →
{𝑎 ∈
(ℕ0 ↑m (1...3)) ∣ ((𝑎‘1) = 1 ∧ (𝑎‘3) = 1)} ∈
(Dioph‘3)) |
| 101 | 93, 99, 100 | mp2an 692 |
. . . . . 6
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ ((𝑎‘1) = 1 ∧ (𝑎‘3) = 1)} ∈
(Dioph‘3) |
| 102 | | expdiophlem2 43034 |
. . . . . 6
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))} ∈
(Dioph‘3) |
| 103 | | orrabdioph 42792 |
. . . . . 6
⊢ (({𝑎 ∈ (ℕ0
↑m (1...3)) ∣ ((𝑎‘1) = 1 ∧ (𝑎‘3) = 1)} ∈ (Dioph‘3) ∧
{𝑎 ∈
(ℕ0 ↑m (1...3)) ∣ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))} ∈ (Dioph‘3)) →
{𝑎 ∈
(ℕ0 ↑m (1...3)) ∣ (((𝑎‘1) = 1 ∧ (𝑎‘3) = 1) ∨ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))))} ∈
(Dioph‘3)) |
| 104 | 101, 102,
103 | mp2an 692 |
. . . . 5
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (((𝑎‘1) = 1 ∧ (𝑎‘3) = 1) ∨ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))))} ∈
(Dioph‘3) |
| 105 | | eq0rabdioph 42787 |
. . . . . . 7
⊢ ((3
∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑m (1...3))
↦ (𝑎‘1)) ∈
(mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (𝑎‘1) = 0} ∈
(Dioph‘3)) |
| 106 | 81, 88, 105 | mp2an 692 |
. . . . . 6
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (𝑎‘1) = 0} ∈
(Dioph‘3) |
| 107 | | eq0rabdioph 42787 |
. . . . . . 7
⊢ ((3
∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑m (1...3))
↦ (𝑎‘3)) ∈
(mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (𝑎‘3) = 0} ∈
(Dioph‘3)) |
| 108 | 81, 97, 107 | mp2an 692 |
. . . . . 6
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (𝑎‘3) = 0} ∈
(Dioph‘3) |
| 109 | | anrabdioph 42791 |
. . . . . 6
⊢ (({𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (𝑎‘1) = 0} ∈ (Dioph‘3) ∧
{𝑎 ∈
(ℕ0 ↑m (1...3)) ∣ (𝑎‘3) = 0} ∈ (Dioph‘3)) →
{𝑎 ∈
(ℕ0 ↑m (1...3)) ∣ ((𝑎‘1) = 0 ∧ (𝑎‘3) = 0)} ∈
(Dioph‘3)) |
| 110 | 106, 108,
109 | mp2an 692 |
. . . . 5
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ ((𝑎‘1) = 0 ∧ (𝑎‘3) = 0)} ∈
(Dioph‘3) |
| 111 | | orrabdioph 42792 |
. . . . 5
⊢ (({𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (((𝑎‘1) = 1 ∧ (𝑎‘3) = 1) ∨ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))))} ∈ (Dioph‘3) ∧
{𝑎 ∈
(ℕ0 ↑m (1...3)) ∣ ((𝑎‘1) = 0 ∧ (𝑎‘3) = 0)} ∈ (Dioph‘3))
→ {𝑎 ∈
(ℕ0 ↑m (1...3)) ∣ ((((𝑎‘1) = 1 ∧ (𝑎‘3) = 1) ∨ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))) ∨ ((𝑎‘1) = 0 ∧ (𝑎‘3) = 0))} ∈
(Dioph‘3)) |
| 112 | 104, 110,
111 | mp2an 692 |
. . . 4
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ ((((𝑎‘1) = 1 ∧ (𝑎‘3) = 1) ∨ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))) ∨ ((𝑎‘1) = 0 ∧ (𝑎‘3) = 0))} ∈
(Dioph‘3) |
| 113 | | anrabdioph 42791 |
. . . 4
⊢ (({𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (𝑎‘2) ∈ ℕ} ∈
(Dioph‘3) ∧ {𝑎
∈ (ℕ0 ↑m (1...3)) ∣ ((((𝑎‘1) = 1 ∧ (𝑎‘3) = 1) ∨ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))) ∨ ((𝑎‘1) = 0 ∧ (𝑎‘3) = 0))} ∈ (Dioph‘3))
→ {𝑎 ∈
(ℕ0 ↑m (1...3)) ∣ ((𝑎‘2) ∈ ℕ ∧ ((((𝑎‘1) = 1 ∧ (𝑎‘3) = 1) ∨ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))) ∨ ((𝑎‘1) = 0 ∧ (𝑎‘3) = 0)))} ∈
(Dioph‘3)) |
| 114 | 86, 112, 113 | mp2an 692 |
. . 3
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ ((𝑎‘2) ∈ ℕ ∧ ((((𝑎‘1) = 1 ∧ (𝑎‘3) = 1) ∨ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))) ∨ ((𝑎‘1) = 0 ∧ (𝑎‘3) = 0)))} ∈
(Dioph‘3) |
| 115 | | eq0rabdioph 42787 |
. . . . 5
⊢ ((3
∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑m (1...3))
↦ (𝑎‘2)) ∈
(mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (𝑎‘2) = 0} ∈
(Dioph‘3)) |
| 116 | 81, 84, 115 | mp2an 692 |
. . . 4
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (𝑎‘2) = 0} ∈
(Dioph‘3) |
| 117 | | anrabdioph 42791 |
. . . 4
⊢ (({𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (𝑎‘2) = 0} ∈ (Dioph‘3) ∧
{𝑎 ∈
(ℕ0 ↑m (1...3)) ∣ (𝑎‘3) = 1} ∈ (Dioph‘3)) →
{𝑎 ∈
(ℕ0 ↑m (1...3)) ∣ ((𝑎‘2) = 0 ∧ (𝑎‘3) = 1)} ∈
(Dioph‘3)) |
| 118 | 116, 99, 117 | mp2an 692 |
. . 3
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ ((𝑎‘2) = 0 ∧ (𝑎‘3) = 1)} ∈
(Dioph‘3) |
| 119 | | orrabdioph 42792 |
. . 3
⊢ (({𝑎 ∈ (ℕ0
↑m (1...3)) ∣ ((𝑎‘2) ∈ ℕ ∧ ((((𝑎‘1) = 1 ∧ (𝑎‘3) = 1) ∨ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))) ∨ ((𝑎‘1) = 0 ∧ (𝑎‘3) = 0)))} ∈ (Dioph‘3)
∧ {𝑎 ∈
(ℕ0 ↑m (1...3)) ∣ ((𝑎‘2) = 0 ∧ (𝑎‘3) = 1)} ∈ (Dioph‘3))
→ {𝑎 ∈
(ℕ0 ↑m (1...3)) ∣ (((𝑎‘2) ∈ ℕ ∧ ((((𝑎‘1) = 1 ∧ (𝑎‘3) = 1) ∨ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))) ∨ ((𝑎‘1) = 0 ∧ (𝑎‘3) = 0))) ∨ ((𝑎‘2) = 0 ∧ (𝑎‘3) = 1))} ∈
(Dioph‘3)) |
| 120 | 114, 118,
119 | mp2an 692 |
. 2
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (((𝑎‘2) ∈ ℕ ∧ ((((𝑎‘1) = 1 ∧ (𝑎‘3) = 1) ∨ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))) ∨ ((𝑎‘1) = 0 ∧ (𝑎‘3) = 0))) ∨ ((𝑎‘2) = 0 ∧ (𝑎‘3) = 1))} ∈
(Dioph‘3) |
| 121 | 80, 120 | eqeltri 2837 |
1
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))} ∈
(Dioph‘3) |