Step | Hyp | Ref
| Expression |
1 | | nq0nn 6425 |
. 2
⊢ (A ∈
Q0 → ∃w∃v((w ∈ 𝜔 ∧
v ∈
N) ∧ A = [〈w,
v〉] ~Q0
)) |
2 | | df-0nq0 6409 |
. . . . . 6
⊢
0Q0 = [〈∅,
1𝑜〉] ~Q0 |
3 | | oveq12 5464 |
. . . . . 6
⊢
((0Q0 = [〈∅,
1𝑜〉] ~Q0 ∧ A =
[〈w, v〉] ~Q0 ) →
(0Q0 ·Q0 A) = ([〈∅, 1𝑜〉]
~Q0 ·Q0
[〈w, v〉] ~Q0
)) |
4 | 2, 3 | mpan 400 |
. . . . 5
⊢ (A = [〈w,
v〉] ~Q0
→ (0Q0 ·Q0
A) = ([〈∅,
1𝑜〉] ~Q0
·Q0 [〈w, v〉]
~Q0 )) |
5 | | peano1 4260 |
. . . . . 6
⊢ ∅
∈ 𝜔 |
6 | | 1pi 6299 |
. . . . . 6
⊢
1𝑜 ∈
N |
7 | | mulnnnq0 6433 |
. . . . . 6
⊢
(((∅ ∈ 𝜔 ∧ 1𝑜 ∈ N) ∧ (w ∈ 𝜔 ∧
v ∈
N)) → ([〈∅, 1𝑜〉]
~Q0 ·Q0
[〈w, v〉] ~Q0 ) =
[〈(∅ ·𝑜 w), (1𝑜
·𝑜 v)〉]
~Q0 ) |
8 | 5, 6, 7 | mpanl12 412 |
. . . . 5
⊢
((w ∈ 𝜔 ∧
v ∈
N) → ([〈∅, 1𝑜〉]
~Q0 ·Q0
[〈w, v〉] ~Q0 ) =
[〈(∅ ·𝑜 w), (1𝑜
·𝑜 v)〉]
~Q0 ) |
9 | 4, 8 | sylan9eqr 2091 |
. . . 4
⊢
(((w ∈ 𝜔 ∧
v ∈
N) ∧ A = [〈w,
v〉] ~Q0 )
→ (0Q0 ·Q0
A) = [〈(∅
·𝑜 w),
(1𝑜 ·𝑜 v)〉] ~Q0
) |
10 | | nnm0r 5997 |
. . . . . . . . . . 11
⊢ (w ∈ 𝜔
→ (∅ ·𝑜 w) = ∅) |
11 | 10 | oveq1d 5470 |
. . . . . . . . . 10
⊢ (w ∈ 𝜔
→ ((∅ ·𝑜 w) ·𝑜
1𝑜) = (∅ ·𝑜
1𝑜)) |
12 | | 1onn 6029 |
. . . . . . . . . . 11
⊢
1𝑜 ∈
𝜔 |
13 | | nnm0r 5997 |
. . . . . . . . . . 11
⊢
(1𝑜 ∈ 𝜔
→ (∅ ·𝑜 1𝑜) =
∅) |
14 | 12, 13 | ax-mp 7 |
. . . . . . . . . 10
⊢ (∅
·𝑜 1𝑜) = ∅ |
15 | 11, 14 | syl6eq 2085 |
. . . . . . . . 9
⊢ (w ∈ 𝜔
→ ((∅ ·𝑜 w) ·𝑜
1𝑜) = ∅) |
16 | 15 | adantr 261 |
. . . . . . . 8
⊢
((w ∈ 𝜔 ∧
v ∈
N) → ((∅ ·𝑜 w) ·𝑜
1𝑜) = ∅) |
17 | | mulpiord 6301 |
. . . . . . . . . . . 12
⊢
((1𝑜 ∈
N ∧ v ∈
N) → (1𝑜
·N v) =
(1𝑜 ·𝑜 v)) |
18 | | mulclpi 6312 |
. . . . . . . . . . . 12
⊢
((1𝑜 ∈
N ∧ v ∈
N) → (1𝑜
·N v) ∈ N) |
19 | 17, 18 | eqeltrrd 2112 |
. . . . . . . . . . 11
⊢
((1𝑜 ∈
N ∧ v ∈
N) → (1𝑜 ·𝑜
v) ∈
N) |
20 | 6, 19 | mpan 400 |
. . . . . . . . . 10
⊢ (v ∈
N → (1𝑜 ·𝑜
v) ∈
N) |
21 | | pinn 6293 |
. . . . . . . . . 10
⊢
((1𝑜 ·𝑜 v) ∈
N → (1𝑜 ·𝑜
v) ∈
𝜔) |
22 | | nnm0 5993 |
. . . . . . . . . 10
⊢
((1𝑜 ·𝑜 v) ∈ 𝜔
→ ((1𝑜 ·𝑜 v) ·𝑜 ∅) =
∅) |
23 | 20, 21, 22 | 3syl 17 |
. . . . . . . . 9
⊢ (v ∈
N → ((1𝑜 ·𝑜
v) ·𝑜 ∅) =
∅) |
24 | 23 | adantl 262 |
. . . . . . . 8
⊢
((w ∈ 𝜔 ∧
v ∈
N) → ((1𝑜 ·𝑜
v) ·𝑜 ∅) =
∅) |
25 | 16, 24 | eqtr4d 2072 |
. . . . . . 7
⊢
((w ∈ 𝜔 ∧
v ∈
N) → ((∅ ·𝑜 w) ·𝑜
1𝑜) = ((1𝑜 ·𝑜
v) ·𝑜
∅)) |
26 | 10, 5 | syl6eqel 2125 |
. . . . . . . 8
⊢ (w ∈ 𝜔
→ (∅ ·𝑜 w) ∈
𝜔) |
27 | | enq0eceq 6420 |
. . . . . . . . 9
⊢
((((∅ ·𝑜 w) ∈ 𝜔
∧ (1𝑜
·𝑜 v) ∈ N) ∧ (∅ ∈
𝜔 ∧ 1𝑜 ∈ N)) → ([〈(∅
·𝑜 w),
(1𝑜 ·𝑜 v)〉] ~Q0 =
[〈∅, 1𝑜〉] ~Q0
↔ ((∅ ·𝑜 w) ·𝑜
1𝑜) = ((1𝑜 ·𝑜
v) ·𝑜
∅))) |
28 | 5, 6, 27 | mpanr12 415 |
. . . . . . . 8
⊢
(((∅ ·𝑜 w) ∈ 𝜔
∧ (1𝑜
·𝑜 v) ∈ N) → ([〈(∅
·𝑜 w),
(1𝑜 ·𝑜 v)〉] ~Q0 =
[〈∅, 1𝑜〉] ~Q0
↔ ((∅ ·𝑜 w) ·𝑜
1𝑜) = ((1𝑜 ·𝑜
v) ·𝑜
∅))) |
29 | 26, 20, 28 | syl2an 273 |
. . . . . . 7
⊢
((w ∈ 𝜔 ∧
v ∈
N) → ([〈(∅ ·𝑜 w), (1𝑜
·𝑜 v)〉]
~Q0 = [〈∅, 1𝑜〉]
~Q0 ↔ ((∅ ·𝑜
w) ·𝑜
1𝑜) = ((1𝑜 ·𝑜
v) ·𝑜
∅))) |
30 | 25, 29 | mpbird 156 |
. . . . . 6
⊢
((w ∈ 𝜔 ∧
v ∈
N) → [〈(∅ ·𝑜 w), (1𝑜
·𝑜 v)〉]
~Q0 = [〈∅, 1𝑜〉]
~Q0 ) |
31 | 30, 2 | syl6eqr 2087 |
. . . . 5
⊢
((w ∈ 𝜔 ∧
v ∈
N) → [〈(∅ ·𝑜 w), (1𝑜
·𝑜 v)〉]
~Q0 = 0Q0) |
32 | 31 | adantr 261 |
. . . 4
⊢
(((w ∈ 𝜔 ∧
v ∈
N) ∧ A = [〈w,
v〉] ~Q0 )
→ [〈(∅ ·𝑜 w), (1𝑜
·𝑜 v)〉]
~Q0 = 0Q0) |
33 | 9, 32 | eqtrd 2069 |
. . 3
⊢
(((w ∈ 𝜔 ∧
v ∈
N) ∧ A = [〈w,
v〉] ~Q0 )
→ (0Q0 ·Q0
A) =
0Q0) |
34 | 33 | exlimivv 1773 |
. 2
⊢ (∃w∃v((w ∈ 𝜔
∧ v ∈ N) ∧ A =
[〈w, v〉] ~Q0 ) →
(0Q0 ·Q0 A) = 0Q0) |
35 | 1, 34 | syl 14 |
1
⊢ (A ∈
Q0 → (0Q0
·Q0 A) =
0Q0) |