Step | Hyp | Ref
| Expression |
1 | | nq0nn 6540 |
. 2
⊢ (𝐴 ∈
Q0 → ∃𝑧∃𝑤((𝑧 ∈ ω ∧ 𝑤 ∈ N) ∧ 𝐴 = [〈𝑧, 𝑤〉] ~Q0
)) |
2 | | 2onn 6094 |
. . . . . . 7
⊢
2𝑜 ∈ ω |
3 | | 1pi 6413 |
. . . . . . 7
⊢
1𝑜 ∈ N |
4 | | mulnnnq0 6548 |
. . . . . . 7
⊢
(((2𝑜 ∈ ω ∧ 1𝑜
∈ N) ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ N)) →
([〈2𝑜, 1𝑜〉]
~Q0 ·Q0 [〈𝑧, 𝑤〉] ~Q0 ) =
[〈(2𝑜 ·𝑜 𝑧), (1𝑜
·𝑜 𝑤)〉] ~Q0
) |
5 | 2, 3, 4 | mpanl12 412 |
. . . . . 6
⊢ ((𝑧 ∈ ω ∧ 𝑤 ∈ N) →
([〈2𝑜, 1𝑜〉]
~Q0 ·Q0 [〈𝑧, 𝑤〉] ~Q0 ) =
[〈(2𝑜 ·𝑜 𝑧), (1𝑜
·𝑜 𝑤)〉] ~Q0
) |
6 | | nn2m 6099 |
. . . . . . . . 9
⊢ (𝑧 ∈ ω →
(2𝑜 ·𝑜 𝑧) = (𝑧 +𝑜 𝑧)) |
7 | 6 | adantr 261 |
. . . . . . . 8
⊢ ((𝑧 ∈ ω ∧ 𝑤 ∈ N) →
(2𝑜 ·𝑜 𝑧) = (𝑧 +𝑜 𝑧)) |
8 | | pinn 6407 |
. . . . . . . . . 10
⊢ (𝑤 ∈ N →
𝑤 ∈
ω) |
9 | | 1onn 6093 |
. . . . . . . . . . . 12
⊢
1𝑜 ∈ ω |
10 | | nnmcom 6068 |
. . . . . . . . . . . 12
⊢
((1𝑜 ∈ ω ∧ 𝑤 ∈ ω) →
(1𝑜 ·𝑜 𝑤) = (𝑤 ·𝑜
1𝑜)) |
11 | 9, 10 | mpan 400 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ ω →
(1𝑜 ·𝑜 𝑤) = (𝑤 ·𝑜
1𝑜)) |
12 | | nnm1 6097 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ ω → (𝑤 ·𝑜
1𝑜) = 𝑤) |
13 | 11, 12 | eqtrd 2072 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ω →
(1𝑜 ·𝑜 𝑤) = 𝑤) |
14 | 8, 13 | syl 14 |
. . . . . . . . 9
⊢ (𝑤 ∈ N →
(1𝑜 ·𝑜 𝑤) = 𝑤) |
15 | 14 | adantl 262 |
. . . . . . . 8
⊢ ((𝑧 ∈ ω ∧ 𝑤 ∈ N) →
(1𝑜 ·𝑜 𝑤) = 𝑤) |
16 | 7, 15 | opeq12d 3557 |
. . . . . . 7
⊢ ((𝑧 ∈ ω ∧ 𝑤 ∈ N) →
〈(2𝑜 ·𝑜 𝑧), (1𝑜
·𝑜 𝑤)〉 = 〈(𝑧 +𝑜 𝑧), 𝑤〉) |
17 | 16 | eceq1d 6142 |
. . . . . 6
⊢ ((𝑧 ∈ ω ∧ 𝑤 ∈ N) →
[〈(2𝑜 ·𝑜 𝑧), (1𝑜
·𝑜 𝑤)〉] ~Q0 =
[〈(𝑧
+𝑜 𝑧),
𝑤〉]
~Q0 ) |
18 | | nnanq0 6556 |
. . . . . . 7
⊢ ((𝑧 ∈ ω ∧ 𝑧 ∈ ω ∧ 𝑤 ∈ N) →
[〈(𝑧
+𝑜 𝑧),
𝑤〉]
~Q0 = ([〈𝑧, 𝑤〉] ~Q0
+Q0 [〈𝑧, 𝑤〉] ~Q0
)) |
19 | 18 | 3anidm12 1192 |
. . . . . 6
⊢ ((𝑧 ∈ ω ∧ 𝑤 ∈ N) →
[〈(𝑧
+𝑜 𝑧),
𝑤〉]
~Q0 = ([〈𝑧, 𝑤〉] ~Q0
+Q0 [〈𝑧, 𝑤〉] ~Q0
)) |
20 | 5, 17, 19 | 3eqtrd 2076 |
. . . . 5
⊢ ((𝑧 ∈ ω ∧ 𝑤 ∈ N) →
([〈2𝑜, 1𝑜〉]
~Q0 ·Q0 [〈𝑧, 𝑤〉] ~Q0 ) =
([〈𝑧, 𝑤〉]
~Q0 +Q0 [〈𝑧, 𝑤〉] ~Q0
)) |
21 | 20 | adantr 261 |
. . . 4
⊢ (((𝑧 ∈ ω ∧ 𝑤 ∈ N) ∧
𝐴 = [〈𝑧, 𝑤〉] ~Q0 ) →
([〈2𝑜, 1𝑜〉]
~Q0 ·Q0 [〈𝑧, 𝑤〉] ~Q0 ) =
([〈𝑧, 𝑤〉]
~Q0 +Q0 [〈𝑧, 𝑤〉] ~Q0
)) |
22 | | oveq2 5520 |
. . . . . 6
⊢ (𝐴 = [〈𝑧, 𝑤〉] ~Q0 →
([〈2𝑜, 1𝑜〉]
~Q0 ·Q0 𝐴) =
([〈2𝑜, 1𝑜〉]
~Q0 ·Q0 [〈𝑧, 𝑤〉] ~Q0
)) |
23 | | id 19 |
. . . . . . 7
⊢ (𝐴 = [〈𝑧, 𝑤〉] ~Q0 →
𝐴 = [〈𝑧, 𝑤〉] ~Q0
) |
24 | 23, 23 | oveq12d 5530 |
. . . . . 6
⊢ (𝐴 = [〈𝑧, 𝑤〉] ~Q0 →
(𝐴
+Q0 𝐴) = ([〈𝑧, 𝑤〉] ~Q0
+Q0 [〈𝑧, 𝑤〉] ~Q0
)) |
25 | 22, 24 | eqeq12d 2054 |
. . . . 5
⊢ (𝐴 = [〈𝑧, 𝑤〉] ~Q0 →
(([〈2𝑜, 1𝑜〉]
~Q0 ·Q0 𝐴) = (𝐴 +Q0 𝐴) ↔
([〈2𝑜, 1𝑜〉]
~Q0 ·Q0 [〈𝑧, 𝑤〉] ~Q0 ) =
([〈𝑧, 𝑤〉]
~Q0 +Q0 [〈𝑧, 𝑤〉] ~Q0
))) |
26 | 25 | adantl 262 |
. . . 4
⊢ (((𝑧 ∈ ω ∧ 𝑤 ∈ N) ∧
𝐴 = [〈𝑧, 𝑤〉] ~Q0 ) →
(([〈2𝑜, 1𝑜〉]
~Q0 ·Q0 𝐴) = (𝐴 +Q0 𝐴) ↔
([〈2𝑜, 1𝑜〉]
~Q0 ·Q0 [〈𝑧, 𝑤〉] ~Q0 ) =
([〈𝑧, 𝑤〉]
~Q0 +Q0 [〈𝑧, 𝑤〉] ~Q0
))) |
27 | 21, 26 | mpbird 156 |
. . 3
⊢ (((𝑧 ∈ ω ∧ 𝑤 ∈ N) ∧
𝐴 = [〈𝑧, 𝑤〉] ~Q0 ) →
([〈2𝑜, 1𝑜〉]
~Q0 ·Q0 𝐴) = (𝐴 +Q0 𝐴)) |
28 | 27 | exlimivv 1776 |
. 2
⊢
(∃𝑧∃𝑤((𝑧 ∈ ω ∧ 𝑤 ∈ N) ∧ 𝐴 = [〈𝑧, 𝑤〉] ~Q0 ) →
([〈2𝑜, 1𝑜〉]
~Q0 ·Q0 𝐴) = (𝐴 +Q0 𝐴)) |
29 | 1, 28 | syl 14 |
1
⊢ (𝐴 ∈
Q0 → ([〈2𝑜,
1𝑜〉] ~Q0
·Q0 𝐴) = (𝐴 +Q0 𝐴)) |