Step | Hyp | Ref
| Expression |
1 | | nq0nn 6632 |
. 2
⊢ (𝐴 ∈
Q0 → ∃𝑤∃𝑣((𝑤 ∈ ω ∧ 𝑣 ∈ N) ∧ 𝐴 = [〈𝑤, 𝑣〉] ~Q0
)) |
2 | | df-0nq0 6616 |
. . . . . 6
⊢
0Q0 = [〈∅,
1𝑜〉] ~Q0 |
3 | | oveq12 5541 |
. . . . . 6
⊢
((0Q0 = [〈∅,
1𝑜〉] ~Q0 ∧ 𝐴 = [〈𝑤, 𝑣〉] ~Q0 ) →
(0Q0 ·Q0 𝐴) = ([〈∅,
1𝑜〉] ~Q0
·Q0 [〈𝑤, 𝑣〉] ~Q0
)) |
4 | 2, 3 | mpan 414 |
. . . . 5
⊢ (𝐴 = [〈𝑤, 𝑣〉] ~Q0 →
(0Q0 ·Q0 𝐴) = ([〈∅,
1𝑜〉] ~Q0
·Q0 [〈𝑤, 𝑣〉] ~Q0
)) |
5 | | peano1 4335 |
. . . . . 6
⊢ ∅
∈ ω |
6 | | 1pi 6505 |
. . . . . 6
⊢
1𝑜 ∈ N |
7 | | mulnnnq0 6640 |
. . . . . 6
⊢
(((∅ ∈ ω ∧ 1𝑜 ∈
N) ∧ (𝑤
∈ ω ∧ 𝑣
∈ N)) → ([〈∅, 1𝑜〉]
~Q0 ·Q0 [〈𝑤, 𝑣〉] ~Q0 ) =
[〈(∅ ·𝑜 𝑤), (1𝑜
·𝑜 𝑣)〉] ~Q0
) |
8 | 5, 6, 7 | mpanl12 426 |
. . . . 5
⊢ ((𝑤 ∈ ω ∧ 𝑣 ∈ N) →
([〈∅, 1𝑜〉] ~Q0
·Q0 [〈𝑤, 𝑣〉] ~Q0 ) =
[〈(∅ ·𝑜 𝑤), (1𝑜
·𝑜 𝑣)〉] ~Q0
) |
9 | 4, 8 | sylan9eqr 2135 |
. . . 4
⊢ (((𝑤 ∈ ω ∧ 𝑣 ∈ N) ∧
𝐴 = [〈𝑤, 𝑣〉] ~Q0 ) →
(0Q0 ·Q0 𝐴) = [〈(∅
·𝑜 𝑤), (1𝑜
·𝑜 𝑣)〉] ~Q0
) |
10 | | nnm0r 6081 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ ω → (∅
·𝑜 𝑤) = ∅) |
11 | 10 | oveq1d 5547 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ω → ((∅
·𝑜 𝑤) ·𝑜
1𝑜) = (∅ ·𝑜
1𝑜)) |
12 | | 1onn 6116 |
. . . . . . . . . . 11
⊢
1𝑜 ∈ ω |
13 | | nnm0r 6081 |
. . . . . . . . . . 11
⊢
(1𝑜 ∈ ω → (∅
·𝑜 1𝑜) = ∅) |
14 | 12, 13 | ax-mp 7 |
. . . . . . . . . 10
⊢ (∅
·𝑜 1𝑜) = ∅ |
15 | 11, 14 | syl6eq 2129 |
. . . . . . . . 9
⊢ (𝑤 ∈ ω → ((∅
·𝑜 𝑤) ·𝑜
1𝑜) = ∅) |
16 | 15 | adantr 270 |
. . . . . . . 8
⊢ ((𝑤 ∈ ω ∧ 𝑣 ∈ N) →
((∅ ·𝑜 𝑤) ·𝑜
1𝑜) = ∅) |
17 | | mulpiord 6507 |
. . . . . . . . . . . 12
⊢
((1𝑜 ∈ N ∧ 𝑣 ∈ N) →
(1𝑜 ·N 𝑣) = (1𝑜
·𝑜 𝑣)) |
18 | | mulclpi 6518 |
. . . . . . . . . . . 12
⊢
((1𝑜 ∈ N ∧ 𝑣 ∈ N) →
(1𝑜 ·N 𝑣) ∈ N) |
19 | 17, 18 | eqeltrrd 2156 |
. . . . . . . . . . 11
⊢
((1𝑜 ∈ N ∧ 𝑣 ∈ N) →
(1𝑜 ·𝑜 𝑣) ∈ N) |
20 | 6, 19 | mpan 414 |
. . . . . . . . . 10
⊢ (𝑣 ∈ N →
(1𝑜 ·𝑜 𝑣) ∈ N) |
21 | | pinn 6499 |
. . . . . . . . . 10
⊢
((1𝑜 ·𝑜 𝑣) ∈ N →
(1𝑜 ·𝑜 𝑣) ∈ ω) |
22 | | nnm0 6077 |
. . . . . . . . . 10
⊢
((1𝑜 ·𝑜 𝑣) ∈ ω →
((1𝑜 ·𝑜 𝑣) ·𝑜 ∅) =
∅) |
23 | 20, 21, 22 | 3syl 17 |
. . . . . . . . 9
⊢ (𝑣 ∈ N →
((1𝑜 ·𝑜 𝑣) ·𝑜 ∅) =
∅) |
24 | 23 | adantl 271 |
. . . . . . . 8
⊢ ((𝑤 ∈ ω ∧ 𝑣 ∈ N) →
((1𝑜 ·𝑜 𝑣) ·𝑜 ∅) =
∅) |
25 | 16, 24 | eqtr4d 2116 |
. . . . . . 7
⊢ ((𝑤 ∈ ω ∧ 𝑣 ∈ N) →
((∅ ·𝑜 𝑤) ·𝑜
1𝑜) = ((1𝑜 ·𝑜
𝑣)
·𝑜 ∅)) |
26 | 10, 5 | syl6eqel 2169 |
. . . . . . . 8
⊢ (𝑤 ∈ ω → (∅
·𝑜 𝑤) ∈ ω) |
27 | | enq0eceq 6627 |
. . . . . . . . 9
⊢
((((∅ ·𝑜 𝑤) ∈ ω ∧ (1𝑜
·𝑜 𝑣) ∈ N) ∧ (∅
∈ ω ∧ 1𝑜 ∈ N)) →
([〈(∅ ·𝑜 𝑤), (1𝑜
·𝑜 𝑣)〉] ~Q0 =
[〈∅, 1𝑜〉] ~Q0
↔ ((∅ ·𝑜 𝑤) ·𝑜
1𝑜) = ((1𝑜 ·𝑜
𝑣)
·𝑜 ∅))) |
28 | 5, 6, 27 | mpanr12 429 |
. . . . . . . 8
⊢
(((∅ ·𝑜 𝑤) ∈ ω ∧ (1𝑜
·𝑜 𝑣) ∈ N) →
([〈(∅ ·𝑜 𝑤), (1𝑜
·𝑜 𝑣)〉] ~Q0 =
[〈∅, 1𝑜〉] ~Q0
↔ ((∅ ·𝑜 𝑤) ·𝑜
1𝑜) = ((1𝑜 ·𝑜
𝑣)
·𝑜 ∅))) |
29 | 26, 20, 28 | syl2an 283 |
. . . . . . 7
⊢ ((𝑤 ∈ ω ∧ 𝑣 ∈ N) →
([〈(∅ ·𝑜 𝑤), (1𝑜
·𝑜 𝑣)〉] ~Q0 =
[〈∅, 1𝑜〉] ~Q0
↔ ((∅ ·𝑜 𝑤) ·𝑜
1𝑜) = ((1𝑜 ·𝑜
𝑣)
·𝑜 ∅))) |
30 | 25, 29 | mpbird 165 |
. . . . . 6
⊢ ((𝑤 ∈ ω ∧ 𝑣 ∈ N) →
[〈(∅ ·𝑜 𝑤), (1𝑜
·𝑜 𝑣)〉] ~Q0 =
[〈∅, 1𝑜〉] ~Q0
) |
31 | 30, 2 | syl6eqr 2131 |
. . . . 5
⊢ ((𝑤 ∈ ω ∧ 𝑣 ∈ N) →
[〈(∅ ·𝑜 𝑤), (1𝑜
·𝑜 𝑣)〉] ~Q0 =
0Q0) |
32 | 31 | adantr 270 |
. . . 4
⊢ (((𝑤 ∈ ω ∧ 𝑣 ∈ N) ∧
𝐴 = [〈𝑤, 𝑣〉] ~Q0 ) →
[〈(∅ ·𝑜 𝑤), (1𝑜
·𝑜 𝑣)〉] ~Q0 =
0Q0) |
33 | 9, 32 | eqtrd 2113 |
. . 3
⊢ (((𝑤 ∈ ω ∧ 𝑣 ∈ N) ∧
𝐴 = [〈𝑤, 𝑣〉] ~Q0 ) →
(0Q0 ·Q0 𝐴) =
0Q0) |
34 | 33 | exlimivv 1817 |
. 2
⊢
(∃𝑤∃𝑣((𝑤 ∈ ω ∧ 𝑣 ∈ N) ∧ 𝐴 = [〈𝑤, 𝑣〉] ~Q0 ) →
(0Q0 ·Q0 𝐴) =
0Q0) |
35 | 1, 34 | syl 14 |
1
⊢ (𝐴 ∈
Q0 → (0Q0
·Q0 𝐴) =
0Q0) |