Step | Hyp | Ref
| Expression |
1 | | enq0er 6533 |
. . 3
⊢
~Q0 Er (ω ×
N) |
2 | 1 | a1i 9 |
. 2
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ ω ∧
𝐶 ∈ N)
→ ~Q0 Er (ω ×
N)) |
3 | | pinn 6407 |
. . . . 5
⊢ (𝐴 ∈ N →
𝐴 ∈
ω) |
4 | 3 | 3ad2ant1 925 |
. . . 4
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ ω ∧
𝐶 ∈ N)
→ 𝐴 ∈
ω) |
5 | | simp2 905 |
. . . 4
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ ω ∧
𝐶 ∈ N)
→ 𝐵 ∈
ω) |
6 | | pinn 6407 |
. . . . 5
⊢ (𝐶 ∈ N →
𝐶 ∈
ω) |
7 | 6 | 3ad2ant3 927 |
. . . 4
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ ω ∧
𝐶 ∈ N)
→ 𝐶 ∈
ω) |
8 | | nnmcom 6068 |
. . . . 5
⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (𝑥 ·𝑜
𝑦) = (𝑦 ·𝑜 𝑥)) |
9 | 8 | adantl 262 |
. . . 4
⊢ (((𝐴 ∈ N ∧
𝐵 ∈ ω ∧
𝐶 ∈ N)
∧ (𝑥 ∈ ω
∧ 𝑦 ∈ ω))
→ (𝑥
·𝑜 𝑦) = (𝑦 ·𝑜 𝑥)) |
10 | | nnmass 6066 |
. . . . 5
⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω ∧ 𝑧 ∈ ω) → ((𝑥 ·𝑜
𝑦)
·𝑜 𝑧) = (𝑥 ·𝑜 (𝑦 ·𝑜
𝑧))) |
11 | 10 | adantl 262 |
. . . 4
⊢ (((𝐴 ∈ N ∧
𝐵 ∈ ω ∧
𝐶 ∈ N)
∧ (𝑥 ∈ ω
∧ 𝑦 ∈ ω
∧ 𝑧 ∈ ω))
→ ((𝑥
·𝑜 𝑦) ·𝑜 𝑧) = (𝑥 ·𝑜 (𝑦 ·𝑜
𝑧))) |
12 | 4, 5, 7, 9, 11 | caov32d 5681 |
. . 3
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ ω ∧
𝐶 ∈ N)
→ ((𝐴
·𝑜 𝐵) ·𝑜 𝐶) = ((𝐴 ·𝑜 𝐶) ·𝑜
𝐵)) |
13 | | nnmcl 6060 |
. . . . . . . 8
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ·𝑜
𝐵) ∈
ω) |
14 | 3, 13 | sylan 267 |
. . . . . . 7
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ ω) →
(𝐴
·𝑜 𝐵) ∈ ω) |
15 | | mulpiord 6415 |
. . . . . . . 8
⊢ ((𝐴 ∈ N ∧
𝐶 ∈ N)
→ (𝐴
·N 𝐶) = (𝐴 ·𝑜 𝐶)) |
16 | | mulclpi 6426 |
. . . . . . . 8
⊢ ((𝐴 ∈ N ∧
𝐶 ∈ N)
→ (𝐴
·N 𝐶) ∈ N) |
17 | 15, 16 | eqeltrrd 2115 |
. . . . . . 7
⊢ ((𝐴 ∈ N ∧
𝐶 ∈ N)
→ (𝐴
·𝑜 𝐶) ∈ N) |
18 | 14, 17 | anim12i 321 |
. . . . . 6
⊢ (((𝐴 ∈ N ∧
𝐵 ∈ ω) ∧
(𝐴 ∈ N
∧ 𝐶 ∈
N)) → ((𝐴 ·𝑜 𝐵) ∈ ω ∧ (𝐴 ·𝑜
𝐶) ∈
N)) |
19 | | simpr 103 |
. . . . . . 7
⊢ (((𝐴 ∈ N ∧
𝐴 ∈ N)
∧ (𝐵 ∈ ω
∧ 𝐶 ∈
N)) → (𝐵
∈ ω ∧ 𝐶
∈ N)) |
20 | 19 | an4s 522 |
. . . . . 6
⊢ (((𝐴 ∈ N ∧
𝐵 ∈ ω) ∧
(𝐴 ∈ N
∧ 𝐶 ∈
N)) → (𝐵
∈ ω ∧ 𝐶
∈ N)) |
21 | 18, 20 | jca 290 |
. . . . 5
⊢ (((𝐴 ∈ N ∧
𝐵 ∈ ω) ∧
(𝐴 ∈ N
∧ 𝐶 ∈
N)) → (((𝐴 ·𝑜 𝐵) ∈ ω ∧ (𝐴 ·𝑜
𝐶) ∈ N)
∧ (𝐵 ∈ ω
∧ 𝐶 ∈
N))) |
22 | 21 | 3impdi 1190 |
. . . 4
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ ω ∧
𝐶 ∈ N)
→ (((𝐴
·𝑜 𝐵) ∈ ω ∧ (𝐴 ·𝑜 𝐶) ∈ N) ∧
(𝐵 ∈ ω ∧
𝐶 ∈
N))) |
23 | | enq0breq 6534 |
. . . 4
⊢ ((((𝐴 ·𝑜
𝐵) ∈ ω ∧
(𝐴
·𝑜 𝐶) ∈ N) ∧ (𝐵 ∈ ω ∧ 𝐶 ∈ N)) →
(〈(𝐴
·𝑜 𝐵), (𝐴 ·𝑜 𝐶)〉
~Q0 〈𝐵, 𝐶〉 ↔ ((𝐴 ·𝑜 𝐵) ·𝑜
𝐶) = ((𝐴 ·𝑜 𝐶) ·𝑜
𝐵))) |
24 | 22, 23 | syl 14 |
. . 3
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ ω ∧
𝐶 ∈ N)
→ (〈(𝐴
·𝑜 𝐵), (𝐴 ·𝑜 𝐶)〉
~Q0 〈𝐵, 𝐶〉 ↔ ((𝐴 ·𝑜 𝐵) ·𝑜
𝐶) = ((𝐴 ·𝑜 𝐶) ·𝑜
𝐵))) |
25 | 12, 24 | mpbird 156 |
. 2
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ ω ∧
𝐶 ∈ N)
→ 〈(𝐴
·𝑜 𝐵), (𝐴 ·𝑜 𝐶)〉
~Q0 〈𝐵, 𝐶〉) |
26 | 2, 25 | erthi 6152 |
1
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ ω ∧
𝐶 ∈ N)
→ [〈(𝐴
·𝑜 𝐵), (𝐴 ·𝑜 𝐶)〉]
~Q0 = [〈𝐵, 𝐶〉] ~Q0
) |