Proof of Theorem expdioph
Step | Hyp | Ref
| Expression |
1 | | pm4.42 1053 |
. . . 4
⊢ ((𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)) ↔ (((𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)) ∧ ¬ (𝑎‘2) ∈ ℕ))) |
2 | | ancom 464 |
. . . . . 6
⊢ (((𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)) ∧ (𝑎‘2) ∈ ℕ) ↔ ((𝑎‘2) ∈ ℕ ∧
(𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))) |
3 | | elmapi 8462 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → 𝑎:(1...3)⟶ℕ0) |
4 | | df-2 11782 |
. . . . . . . . . . . . . . 15
⊢ 2 = (1 +
1) |
5 | | df-3 11783 |
. . . . . . . . . . . . . . . 16
⊢ 3 = (2 +
1) |
6 | | ssid 3900 |
. . . . . . . . . . . . . . . 16
⊢ (1...3)
⊆ (1...3) |
7 | 5, 6 | jm2.27dlem5 40430 |
. . . . . . . . . . . . . . 15
⊢ (1...2)
⊆ (1...3) |
8 | 4, 7 | jm2.27dlem5 40430 |
. . . . . . . . . . . . . 14
⊢ (1...1)
⊆ (1...3) |
9 | | 1nn 11730 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℕ |
10 | 9 | jm2.27dlem3 40428 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
(1...1) |
11 | 8, 10 | sselii 3875 |
. . . . . . . . . . . . 13
⊢ 1 ∈
(1...3) |
12 | | ffvelrn 6862 |
. . . . . . . . . . . . 13
⊢ ((𝑎:(1...3)⟶ℕ0 ∧ 1
∈ (1...3)) → (𝑎‘1) ∈
ℕ0) |
13 | 3, 11, 12 | sylancl 589 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → (𝑎‘1) ∈
ℕ0) |
14 | 13 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘2) ∈ ℕ) → (𝑎‘1) ∈
ℕ0) |
15 | | elnn0 11981 |
. . . . . . . . . . 11
⊢ ((𝑎‘1) ∈
ℕ0 ↔ ((𝑎‘1) ∈ ℕ ∨ (𝑎‘1) = 0)) |
16 | 14, 15 | sylib 221 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) ∈ ℕ ∨
(𝑎‘1) =
0)) |
17 | | elnn1uz2 12410 |
. . . . . . . . . . . 12
⊢ ((𝑎‘1) ∈ ℕ ↔
((𝑎‘1) = 1 ∨
(𝑎‘1) ∈
(ℤ≥‘2))) |
18 | 17 | biimpi 219 |
. . . . . . . . . . 11
⊢ ((𝑎‘1) ∈ ℕ →
((𝑎‘1) = 1 ∨
(𝑎‘1) ∈
(ℤ≥‘2))) |
19 | 18 | orim1i 909 |
. . . . . . . . . 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 536 |
. . . . . . . 8
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)) ↔ ((((𝑎‘1) = 1 ∨ (𝑎‘1) ∈
(ℤ≥‘2)) ∨ (𝑎‘1) = 0) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))))) |
22 | | andir 1008 |
. . . . . . . . . 10
⊢
(((((𝑎‘1) = 1
∨ (𝑎‘1) ∈
(ℤ≥‘2)) ∨ (𝑎‘1) = 0) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))) ↔ ((((𝑎‘1) = 1 ∨ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))) ∨ ((𝑎‘1) = 0 ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))))) |
23 | | andir 1008 |
. . . . . . . . . . 11
⊢ ((((𝑎‘1) = 1 ∨ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))) ↔ (((𝑎‘1) = 1 ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))) ∨ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))))) |
24 | 23 | orbi1i 913 |
. . . . . . . . . 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 278 |
. . . . . . . . 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 12088 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎‘2) ∈ ℕ →
(𝑎‘2) ∈
ℤ) |
27 | | 1exp 13553 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎‘2) ∈ ℤ →
(1↑(𝑎‘2)) =
1) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎‘2) ∈ ℕ →
(1↑(𝑎‘2)) =
1) |
29 | 28 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘2) ∈ ℕ) →
(1↑(𝑎‘2)) =
1) |
30 | 29 | eqeq2d 2750 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘3) = (1↑(𝑎‘2)) ↔ (𝑎‘3) = 1)) |
31 | | oveq1 7180 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎‘1) = 1 → ((𝑎‘1)↑(𝑎‘2)) = (1↑(𝑎‘2))) |
32 | 31 | eqeq2d 2750 |
. . . . . . . . . . . . . 14
⊢ ((𝑎‘1) = 1 → ((𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)) ↔ (𝑎‘3) = (1↑(𝑎‘2)))) |
33 | 32 | bibi1d 347 |
. . . . . . . . . . . . 13
⊢ ((𝑎‘1) = 1 → (((𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)) ↔ (𝑎‘3) = 1) ↔ ((𝑎‘3) = (1↑(𝑎‘2)) ↔ (𝑎‘3) = 1))) |
34 | 30, 33 | syl5ibrcom 250 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) = 1 → ((𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)) ↔ (𝑎‘3) = 1))) |
35 | 34 | pm5.32d 580 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘2) ∈ ℕ) → (((𝑎‘1) = 1 ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))) ↔ ((𝑎‘1) = 1 ∧ (𝑎‘3) = 1))) |
36 | | iba 531 |
. . . . . . . . . . . . 13
⊢ ((𝑎‘2) ∈ ℕ →
((𝑎‘1) ∈
(ℤ≥‘2) ↔ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ))) |
37 | 36 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) ∈
(ℤ≥‘2) ↔ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ))) |
38 | 37 | anbi1d 633 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘2) ∈ ℕ) → (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))) ↔ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))))) |
39 | 35, 38 | orbi12d 918 |
. . . . . . . . . 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 13559 |
. . . . . . . . . . . . . 14
⊢ ((𝑎‘2) ∈ ℕ →
(0↑(𝑎‘2)) =
0) |
41 | 40 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘2) ∈ ℕ) →
(0↑(𝑎‘2)) =
0) |
42 | 41 | eqeq2d 2750 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘3) = (0↑(𝑎‘2)) ↔ (𝑎‘3) = 0)) |
43 | | oveq1 7180 |
. . . . . . . . . . . . . 14
⊢ ((𝑎‘1) = 0 → ((𝑎‘1)↑(𝑎‘2)) = (0↑(𝑎‘2))) |
44 | 43 | eqeq2d 2750 |
. . . . . . . . . . . . 13
⊢ ((𝑎‘1) = 0 → ((𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)) ↔ (𝑎‘3) = (0↑(𝑎‘2)))) |
45 | 44 | bibi1d 347 |
. . . . . . . . . . . 12
⊢ ((𝑎‘1) = 0 → (((𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)) ↔ (𝑎‘3) = 0) ↔ ((𝑎‘3) = (0↑(𝑎‘2)) ↔ (𝑎‘3) = 0))) |
46 | 42, 45 | syl5ibrcom 250 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) = 0 → ((𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)) ↔ (𝑎‘3) = 0))) |
47 | 46 | pm5.32d 580 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘2) ∈ ℕ) → (((𝑎‘1) = 0 ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))) ↔ ((𝑎‘1) = 0 ∧ (𝑎‘3) = 0))) |
48 | 39, 47 | orbi12d 918 |
. . . . . . . . 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 | syl5bb 286 |
. . . . . . . 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 282 |
. . . . . . 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 582 |
. . . . . 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 | syl5bb 286 |
. . . . 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 464 |
. . . . . 6
⊢ (((𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)) ∧ ¬ (𝑎‘2) ∈ ℕ) ↔ (¬
(𝑎‘2) ∈ ℕ
∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))) |
54 | | 2nn 11792 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℕ |
55 | 54 | jm2.27dlem3 40428 |
. . . . . . . . . . 11
⊢ 2 ∈
(1...2) |
56 | 7, 55 | sselii 3875 |
. . . . . . . . . 10
⊢ 2 ∈
(1...3) |
57 | | ffvelrn 6862 |
. . . . . . . . . 10
⊢ ((𝑎:(1...3)⟶ℕ0 ∧ 2
∈ (1...3)) → (𝑎‘2) ∈
ℕ0) |
58 | 3, 56, 57 | sylancl 589 |
. . . . . . . . 9
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → (𝑎‘2) ∈
ℕ0) |
59 | | elnn0 11981 |
. . . . . . . . . . 11
⊢ ((𝑎‘2) ∈
ℕ0 ↔ ((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0)) |
60 | | pm2.53 850 |
. . . . . . . . . . 11
⊢ (((𝑎‘2) ∈ ℕ ∨
(𝑎‘2) = 0) →
(¬ (𝑎‘2) ∈
ℕ → (𝑎‘2)
= 0)) |
61 | 59, 60 | sylbi 220 |
. . . . . . . . . 10
⊢ ((𝑎‘2) ∈
ℕ0 → (¬ (𝑎‘2) ∈ ℕ → (𝑎‘2) = 0)) |
62 | | 0nnn 11755 |
. . . . . . . . . . 11
⊢ ¬ 0
∈ ℕ |
63 | | eleq1 2821 |
. . . . . . . . . . 11
⊢ ((𝑎‘2) = 0 → ((𝑎‘2) ∈ ℕ ↔
0 ∈ ℕ)) |
64 | 62, 63 | mtbiri 330 |
. . . . . . . . . 10
⊢ ((𝑎‘2) = 0 → ¬
(𝑎‘2) ∈
ℕ) |
65 | 61, 64 | impbid1 228 |
. . . . . . . . 9
⊢ ((𝑎‘2) ∈
ℕ0 → (¬ (𝑎‘2) ∈ ℕ ↔ (𝑎‘2) = 0)) |
66 | 58, 65 | syl 17 |
. . . . . . . 8
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → (¬ (𝑎‘2) ∈ ℕ ↔ (𝑎‘2) = 0)) |
67 | 66 | anbi1d 633 |
. . . . . . 7
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → ((¬ (𝑎‘2) ∈ ℕ ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))) ↔ ((𝑎‘2) = 0 ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))))) |
68 | 13 | nn0cnd 12041 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → (𝑎‘1) ∈ ℂ) |
69 | 68 | exp0d 13599 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → ((𝑎‘1)↑0) = 1) |
70 | 69 | eqeq2d 2750 |
. . . . . . . . 9
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → ((𝑎‘3) = ((𝑎‘1)↑0) ↔ (𝑎‘3) = 1)) |
71 | | oveq2 7181 |
. . . . . . . . . . 11
⊢ ((𝑎‘2) = 0 → ((𝑎‘1)↑(𝑎‘2)) = ((𝑎‘1)↑0)) |
72 | 71 | eqeq2d 2750 |
. . . . . . . . . 10
⊢ ((𝑎‘2) = 0 → ((𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)) ↔ (𝑎‘3) = ((𝑎‘1)↑0))) |
73 | 72 | bibi1d 347 |
. . . . . . . . 9
⊢ ((𝑎‘2) = 0 → (((𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)) ↔ (𝑎‘3) = 1) ↔ ((𝑎‘3) = ((𝑎‘1)↑0) ↔ (𝑎‘3) = 1))) |
74 | 70, 73 | syl5ibrcom 250 |
. . . . . . . 8
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → ((𝑎‘2) = 0 → ((𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)) ↔ (𝑎‘3) = 1))) |
75 | 74 | pm5.32d 580 |
. . . . . . 7
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → (((𝑎‘2) = 0 ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))) ↔ ((𝑎‘2) = 0 ∧ (𝑎‘3) = 1))) |
76 | 67, 75 | bitrd 282 |
. . . . . 6
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → ((¬ (𝑎‘2) ∈ ℕ ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))) ↔ ((𝑎‘2) = 0 ∧ (𝑎‘3) = 1))) |
77 | 53, 76 | syl5bb 286 |
. . . . 5
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → (((𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)) ∧ ¬ (𝑎‘2) ∈ ℕ) ↔ ((𝑎‘2) = 0 ∧ (𝑎‘3) =
1))) |
78 | 52, 77 | orbi12d 918 |
. . . 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 | syl5bb 286 |
. . 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 3374 |
. 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 11997 |
. . . . 5
⊢ 3 ∈
ℕ0 |
82 | | ovex 7206 |
. . . . . 6
⊢ (1...3)
∈ V |
83 | | mzpproj 40154 |
. . . . . 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 40224 |
. . . . 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 40154 |
. . . . . . . . 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 12096 |
. . . . . . . . 9
⊢ 1 ∈
ℤ |
90 | | mzpconstmpt 40157 |
. . . . . . . . 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 40194 |
. . . . . . . 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 1462 |
. . . . . . 7
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (𝑎‘1) = 1} ∈
(Dioph‘3) |
94 | | 3nn 11798 |
. . . . . . . . . 10
⊢ 3 ∈
ℕ |
95 | 94 | jm2.27dlem3 40428 |
. . . . . . . . 9
⊢ 3 ∈
(1...3) |
96 | | mzpproj 40154 |
. . . . . . . . 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 40194 |
. . . . . . . 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 1462 |
. . . . . . 7
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (𝑎‘3) = 1} ∈
(Dioph‘3) |
100 | | anrabdioph 40197 |
. . . . . . 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 40439 |
. . . . . 6
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))} ∈
(Dioph‘3) |
103 | | orrabdioph 40198 |
. . . . . 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 40193 |
. . . . . . 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 40193 |
. . . . . . 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 40197 |
. . . . . 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 40198 |
. . . . 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 40197 |
. . . 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 40193 |
. . . . 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 40197 |
. . . 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 40198 |
. . 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 2830 |
1
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))} ∈
(Dioph‘3) |