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
⊢
((A = [〈w, v〉]
~Q0 ∧
0Q0 = [〈∅, 1𝑜〉]
~Q0 ) → (A
+Q0 0Q0) = ([〈w, v〉]
~Q0 +Q0 [〈∅,
1𝑜〉] ~Q0 )) |
4 | 2, 3 | mpan2 401 |
. . . . 5
⊢ (A = [〈w,
v〉] ~Q0
→ (A +Q0
0Q0) = ([〈w,
v〉] ~Q0
+Q0 [〈∅, 1𝑜〉]
~Q0 )) |
5 | | peano1 4260 |
. . . . . 6
⊢ ∅
∈ 𝜔 |
6 | | 1pi 6299 |
. . . . . 6
⊢
1𝑜 ∈
N |
7 | | addnnnq0 6432 |
. . . . . 6
⊢
(((w ∈ 𝜔 ∧
v ∈
N) ∧ (∅ ∈ 𝜔 ∧
1𝑜 ∈ N))
→ ([〈w, v〉] ~Q0
+Q0 [〈∅, 1𝑜〉]
~Q0 ) = [〈((w
·𝑜 1𝑜) +𝑜
(v ·𝑜 ∅)),
(v ·𝑜
1𝑜)〉] ~Q0 ) |
8 | 5, 6, 7 | mpanr12 415 |
. . . . 5
⊢
((w ∈ 𝜔 ∧
v ∈
N) → ([〈w, v〉] ~Q0
+Q0 [〈∅, 1𝑜〉]
~Q0 ) = [〈((w
·𝑜 1𝑜) +𝑜
(v ·𝑜 ∅)),
(v ·𝑜
1𝑜)〉] ~Q0 ) |
9 | 4, 8 | sylan9eqr 2091 |
. . . 4
⊢
(((w ∈ 𝜔 ∧
v ∈
N) ∧ A = [〈w,
v〉] ~Q0 )
→ (A +Q0
0Q0) = [〈((w
·𝑜 1𝑜) +𝑜
(v ·𝑜 ∅)),
(v ·𝑜
1𝑜)〉] ~Q0 ) |
10 | | pinn 6293 |
. . . . . . . . . 10
⊢ (v ∈
N → v ∈ 𝜔) |
11 | | nnm0 5993 |
. . . . . . . . . . 11
⊢ (v ∈ 𝜔
→ (v ·𝑜
∅) = ∅) |
12 | 11 | oveq2d 5471 |
. . . . . . . . . 10
⊢ (v ∈ 𝜔
→ ((w ·𝑜
1𝑜) +𝑜 (v ·𝑜 ∅)) =
((w ·𝑜
1𝑜) +𝑜 ∅)) |
13 | 10, 12 | syl 14 |
. . . . . . . . 9
⊢ (v ∈
N → ((w
·𝑜 1𝑜) +𝑜
(v ·𝑜 ∅)) =
((w ·𝑜
1𝑜) +𝑜 ∅)) |
14 | | nnm1 6033 |
. . . . . . . . . . 11
⊢ (w ∈ 𝜔
→ (w ·𝑜
1𝑜) = w) |
15 | 14 | oveq1d 5470 |
. . . . . . . . . 10
⊢ (w ∈ 𝜔
→ ((w ·𝑜
1𝑜) +𝑜 ∅) = (w +𝑜 ∅)) |
16 | | nna0 5992 |
. . . . . . . . . 10
⊢ (w ∈ 𝜔
→ (w +𝑜 ∅) =
w) |
17 | 15, 16 | eqtrd 2069 |
. . . . . . . . 9
⊢ (w ∈ 𝜔
→ ((w ·𝑜
1𝑜) +𝑜 ∅) = w) |
18 | 13, 17 | sylan9eqr 2091 |
. . . . . . . 8
⊢
((w ∈ 𝜔 ∧
v ∈
N) → ((w
·𝑜 1𝑜) +𝑜
(v ·𝑜 ∅)) =
w) |
19 | | nnm1 6033 |
. . . . . . . . . 10
⊢ (v ∈ 𝜔
→ (v ·𝑜
1𝑜) = v) |
20 | 10, 19 | syl 14 |
. . . . . . . . 9
⊢ (v ∈
N → (v
·𝑜 1𝑜) = v) |
21 | 20 | adantl 262 |
. . . . . . . 8
⊢
((w ∈ 𝜔 ∧
v ∈
N) → (v
·𝑜 1𝑜) = v) |
22 | 18, 21 | opeq12d 3548 |
. . . . . . 7
⊢
((w ∈ 𝜔 ∧
v ∈
N) → 〈((w
·𝑜 1𝑜) +𝑜
(v ·𝑜 ∅)),
(v ·𝑜
1𝑜)〉 = 〈w,
v〉) |
23 | 22 | eceq1d 6078 |
. . . . . 6
⊢
((w ∈ 𝜔 ∧
v ∈
N) → [〈((w
·𝑜 1𝑜) +𝑜
(v ·𝑜 ∅)),
(v ·𝑜
1𝑜)〉] ~Q0 = [〈w, v〉]
~Q0 ) |
24 | 23 | eqeq2d 2048 |
. . . . 5
⊢
((w ∈ 𝜔 ∧
v ∈
N) → (A =
[〈((w ·𝑜
1𝑜) +𝑜 (v ·𝑜 ∅)), (v ·𝑜
1𝑜)〉] ~Q0 ↔ A = [〈w,
v〉] ~Q0
)) |
25 | 24 | biimpar 281 |
. . . 4
⊢
(((w ∈ 𝜔 ∧
v ∈
N) ∧ A = [〈w,
v〉] ~Q0 )
→ A = [〈((w ·𝑜
1𝑜) +𝑜 (v ·𝑜 ∅)), (v ·𝑜
1𝑜)〉] ~Q0 ) |
26 | 9, 25 | eqtr4d 2072 |
. . 3
⊢
(((w ∈ 𝜔 ∧
v ∈
N) ∧ A = [〈w,
v〉] ~Q0 )
→ (A +Q0
0Q0) = A) |
27 | 26 | exlimivv 1773 |
. 2
⊢ (∃w∃v((w ∈ 𝜔
∧ v ∈ N) ∧ A =
[〈w, v〉] ~Q0 ) →
(A +Q0
0Q0) = A) |
28 | 1, 27 | syl 14 |
1
⊢ (A ∈
Q0 → (A
+Q0 0Q0) = A) |