Step | Hyp | Ref
| Expression |
1 | | nqpi 6476 |
. . . 4
⊢ (𝐴 ∈ Q →
∃𝑥∃𝑦((𝑥 ∈ N ∧ 𝑦 ∈ N) ∧
𝐴 = [〈𝑥, 𝑦〉] ~Q
)) |
2 | | nq0nn 6540 |
. . . 4
⊢ (𝐵 ∈
Q0 → ∃𝑧∃𝑤((𝑧 ∈ ω ∧ 𝑤 ∈ N) ∧ 𝐵 = [〈𝑧, 𝑤〉] ~Q0
)) |
3 | 1, 2 | anim12i 321 |
. . 3
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈
Q0) → (∃𝑥∃𝑦((𝑥 ∈ N ∧ 𝑦 ∈ N) ∧
𝐴 = [〈𝑥, 𝑦〉] ~Q ) ∧
∃𝑧∃𝑤((𝑧 ∈ ω ∧ 𝑤 ∈ N) ∧ 𝐵 = [〈𝑧, 𝑤〉] ~Q0
))) |
4 | | ee4anv 1809 |
. . 3
⊢
(∃𝑥∃𝑦∃𝑧∃𝑤(((𝑥 ∈ N ∧ 𝑦 ∈ N) ∧
𝐴 = [〈𝑥, 𝑦〉] ~Q ) ∧
((𝑧 ∈ ω ∧
𝑤 ∈ N)
∧ 𝐵 = [〈𝑧, 𝑤〉] ~Q0 ))
↔ (∃𝑥∃𝑦((𝑥 ∈ N ∧ 𝑦 ∈ N) ∧
𝐴 = [〈𝑥, 𝑦〉] ~Q ) ∧
∃𝑧∃𝑤((𝑧 ∈ ω ∧ 𝑤 ∈ N) ∧ 𝐵 = [〈𝑧, 𝑤〉] ~Q0
))) |
5 | 3, 4 | sylibr 137 |
. 2
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈
Q0) → ∃𝑥∃𝑦∃𝑧∃𝑤(((𝑥 ∈ N ∧ 𝑦 ∈ N) ∧
𝐴 = [〈𝑥, 𝑦〉] ~Q ) ∧
((𝑧 ∈ ω ∧
𝑤 ∈ N)
∧ 𝐵 = [〈𝑧, 𝑤〉] ~Q0
))) |
6 | | oveq12 5521 |
. . . . . . 7
⊢ ((𝐴 = [〈𝑥, 𝑦〉] ~Q ∧
𝐵 = [〈𝑧, 𝑤〉] ~Q0 ) →
(𝐴
+Q0 𝐵) = ([〈𝑥, 𝑦〉] ~Q
+Q0 [〈𝑧, 𝑤〉] ~Q0
)) |
7 | 6 | ad2ant2l 477 |
. . . . . 6
⊢ ((((𝑥 ∈ N ∧
𝑦 ∈ N)
∧ 𝐴 = [〈𝑥, 𝑦〉] ~Q ) ∧
((𝑧 ∈ ω ∧
𝑤 ∈ N)
∧ 𝐵 = [〈𝑧, 𝑤〉] ~Q0 ))
→ (𝐴
+Q0 𝐵) = ([〈𝑥, 𝑦〉] ~Q
+Q0 [〈𝑧, 𝑤〉] ~Q0
)) |
8 | | nqnq0pi 6536 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ N ∧
𝑦 ∈ N)
→ [〈𝑥, 𝑦〉]
~Q0 = [〈𝑥, 𝑦〉] ~Q
) |
9 | 8 | oveq1d 5527 |
. . . . . . . . 9
⊢ ((𝑥 ∈ N ∧
𝑦 ∈ N)
→ ([〈𝑥, 𝑦〉]
~Q0 +Q0 [〈𝑧, 𝑤〉] ~Q0 ) =
([〈𝑥, 𝑦〉]
~Q +Q0 [〈𝑧, 𝑤〉] ~Q0
)) |
10 | 9 | adantr 261 |
. . . . . . . 8
⊢ (((𝑥 ∈ N ∧
𝑦 ∈ N)
∧ (𝑧 ∈ ω
∧ 𝑤 ∈
N)) → ([〈𝑥, 𝑦〉] ~Q0
+Q0 [〈𝑧, 𝑤〉] ~Q0 ) =
([〈𝑥, 𝑦〉]
~Q +Q0 [〈𝑧, 𝑤〉] ~Q0
)) |
11 | | pinn 6407 |
. . . . . . . . 9
⊢ (𝑥 ∈ N →
𝑥 ∈
ω) |
12 | | addnnnq0 6547 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ω ∧ 𝑦 ∈ N) ∧
(𝑧 ∈ ω ∧
𝑤 ∈ N))
→ ([〈𝑥, 𝑦〉]
~Q0 +Q0 [〈𝑧, 𝑤〉] ~Q0 ) =
[〈((𝑥
·𝑜 𝑤) +𝑜 (𝑦 ·𝑜 𝑧)), (𝑦 ·𝑜 𝑤)〉]
~Q0 ) |
13 | 11, 12 | sylanl1 382 |
. . . . . . . 8
⊢ (((𝑥 ∈ N ∧
𝑦 ∈ N)
∧ (𝑧 ∈ ω
∧ 𝑤 ∈
N)) → ([〈𝑥, 𝑦〉] ~Q0
+Q0 [〈𝑧, 𝑤〉] ~Q0 ) =
[〈((𝑥
·𝑜 𝑤) +𝑜 (𝑦 ·𝑜 𝑧)), (𝑦 ·𝑜 𝑤)〉]
~Q0 ) |
14 | 10, 13 | eqtr3d 2074 |
. . . . . . 7
⊢ (((𝑥 ∈ N ∧
𝑦 ∈ N)
∧ (𝑧 ∈ ω
∧ 𝑤 ∈
N)) → ([〈𝑥, 𝑦〉] ~Q
+Q0 [〈𝑧, 𝑤〉] ~Q0 ) =
[〈((𝑥
·𝑜 𝑤) +𝑜 (𝑦 ·𝑜 𝑧)), (𝑦 ·𝑜 𝑤)〉]
~Q0 ) |
15 | 14 | ad2ant2r 478 |
. . . . . 6
⊢ ((((𝑥 ∈ N ∧
𝑦 ∈ N)
∧ 𝐴 = [〈𝑥, 𝑦〉] ~Q ) ∧
((𝑧 ∈ ω ∧
𝑤 ∈ N)
∧ 𝐵 = [〈𝑧, 𝑤〉] ~Q0 ))
→ ([〈𝑥, 𝑦〉]
~Q +Q0 [〈𝑧, 𝑤〉] ~Q0 ) =
[〈((𝑥
·𝑜 𝑤) +𝑜 (𝑦 ·𝑜 𝑧)), (𝑦 ·𝑜 𝑤)〉]
~Q0 ) |
16 | 7, 15 | eqtrd 2072 |
. . . . 5
⊢ ((((𝑥 ∈ N ∧
𝑦 ∈ N)
∧ 𝐴 = [〈𝑥, 𝑦〉] ~Q ) ∧
((𝑧 ∈ ω ∧
𝑤 ∈ N)
∧ 𝐵 = [〈𝑧, 𝑤〉] ~Q0 ))
→ (𝐴
+Q0 𝐵) = [〈((𝑥 ·𝑜 𝑤) +𝑜 (𝑦 ·𝑜
𝑧)), (𝑦 ·𝑜 𝑤)〉]
~Q0 ) |
17 | | pinn 6407 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ N →
𝑦 ∈
ω) |
18 | | nnmcl 6060 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ω ∧ 𝑧 ∈ ω) → (𝑦 ·𝑜
𝑧) ∈
ω) |
19 | 17, 18 | sylan 267 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ N ∧
𝑧 ∈ ω) →
(𝑦
·𝑜 𝑧) ∈ ω) |
20 | 19 | ad2ant2lr 479 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ N ∧
𝑦 ∈ N)
∧ (𝑧 ∈ ω
∧ 𝑤 ∈
N)) → (𝑦
·𝑜 𝑧) ∈ ω) |
21 | | mulpiord 6415 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ N ∧
𝑤 ∈ N)
→ (𝑥
·N 𝑤) = (𝑥 ·𝑜 𝑤)) |
22 | | mulclpi 6426 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ N ∧
𝑤 ∈ N)
→ (𝑥
·N 𝑤) ∈ N) |
23 | 21, 22 | eqeltrrd 2115 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ N ∧
𝑤 ∈ N)
→ (𝑥
·𝑜 𝑤) ∈ N) |
24 | 23 | ad2ant2rl 480 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ N ∧
𝑦 ∈ N)
∧ (𝑧 ∈ ω
∧ 𝑤 ∈
N)) → (𝑥
·𝑜 𝑤) ∈ N) |
25 | | pinn 6407 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ·𝑜
𝑤) ∈ N
→ (𝑥
·𝑜 𝑤) ∈ ω) |
26 | | nnacom 6063 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ·𝑜
𝑧) ∈ ω ∧
(𝑥
·𝑜 𝑤) ∈ ω) → ((𝑦 ·𝑜 𝑧) +𝑜 (𝑥 ·𝑜
𝑤)) = ((𝑥 ·𝑜 𝑤) +𝑜 (𝑦 ·𝑜
𝑧))) |
27 | 25, 26 | sylan2 270 |
. . . . . . . . . . . 12
⊢ (((𝑦 ·𝑜
𝑧) ∈ ω ∧
(𝑥
·𝑜 𝑤) ∈ N) → ((𝑦 ·𝑜
𝑧) +𝑜
(𝑥
·𝑜 𝑤)) = ((𝑥 ·𝑜 𝑤) +𝑜 (𝑦 ·𝑜
𝑧))) |
28 | 20, 24, 27 | syl2anc 391 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ N ∧
𝑦 ∈ N)
∧ (𝑧 ∈ ω
∧ 𝑤 ∈
N)) → ((𝑦 ·𝑜 𝑧) +𝑜 (𝑥 ·𝑜
𝑤)) = ((𝑥 ·𝑜 𝑤) +𝑜 (𝑦 ·𝑜
𝑧))) |
29 | | nnppipi 6441 |
. . . . . . . . . . . 12
⊢ (((𝑦 ·𝑜
𝑧) ∈ ω ∧
(𝑥
·𝑜 𝑤) ∈ N) → ((𝑦 ·𝑜
𝑧) +𝑜
(𝑥
·𝑜 𝑤)) ∈ N) |
30 | 20, 24, 29 | syl2anc 391 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ N ∧
𝑦 ∈ N)
∧ (𝑧 ∈ ω
∧ 𝑤 ∈
N)) → ((𝑦 ·𝑜 𝑧) +𝑜 (𝑥 ·𝑜
𝑤)) ∈
N) |
31 | 28, 30 | eqeltrrd 2115 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ N ∧
𝑦 ∈ N)
∧ (𝑧 ∈ ω
∧ 𝑤 ∈
N)) → ((𝑥 ·𝑜 𝑤) +𝑜 (𝑦 ·𝑜
𝑧)) ∈
N) |
32 | | mulpiord 6415 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ N ∧
𝑤 ∈ N)
→ (𝑦
·N 𝑤) = (𝑦 ·𝑜 𝑤)) |
33 | | mulclpi 6426 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ N ∧
𝑤 ∈ N)
→ (𝑦
·N 𝑤) ∈ N) |
34 | 32, 33 | eqeltrrd 2115 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ N ∧
𝑤 ∈ N)
→ (𝑦
·𝑜 𝑤) ∈ N) |
35 | 34 | ad2ant2l 477 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ N ∧
𝑦 ∈ N)
∧ (𝑧 ∈ ω
∧ 𝑤 ∈
N)) → (𝑦
·𝑜 𝑤) ∈ N) |
36 | | opelxpi 4376 |
. . . . . . . . . 10
⊢ ((((𝑥 ·𝑜
𝑤) +𝑜
(𝑦
·𝑜 𝑧)) ∈ N ∧ (𝑦 ·𝑜
𝑤) ∈ N)
→ 〈((𝑥
·𝑜 𝑤) +𝑜 (𝑦 ·𝑜 𝑧)), (𝑦 ·𝑜 𝑤)〉 ∈ (N
× N)) |
37 | 31, 35, 36 | syl2anc 391 |
. . . . . . . . 9
⊢ (((𝑥 ∈ N ∧
𝑦 ∈ N)
∧ (𝑧 ∈ ω
∧ 𝑤 ∈
N)) → 〈((𝑥 ·𝑜 𝑤) +𝑜 (𝑦 ·𝑜
𝑧)), (𝑦 ·𝑜 𝑤)〉 ∈ (N
× N)) |
38 | | enqex 6458 |
. . . . . . . . . 10
⊢
~Q ∈ V |
39 | 38 | ecelqsi 6160 |
. . . . . . . . 9
⊢
(〈((𝑥
·𝑜 𝑤) +𝑜 (𝑦 ·𝑜 𝑧)), (𝑦 ·𝑜 𝑤)〉 ∈ (N
× N) → [〈((𝑥 ·𝑜 𝑤) +𝑜 (𝑦 ·𝑜
𝑧)), (𝑦 ·𝑜 𝑤)〉]
~Q ∈ ((N × N)
/ ~Q )) |
40 | 37, 39 | syl 14 |
. . . . . . . 8
⊢ (((𝑥 ∈ N ∧
𝑦 ∈ N)
∧ (𝑧 ∈ ω
∧ 𝑤 ∈
N)) → [〈((𝑥 ·𝑜 𝑤) +𝑜 (𝑦 ·𝑜
𝑧)), (𝑦 ·𝑜 𝑤)〉]
~Q ∈ ((N × N)
/ ~Q )) |
41 | | df-nqqs 6446 |
. . . . . . . 8
⊢
Q = ((N × N) /
~Q ) |
42 | 40, 41 | syl6eleqr 2131 |
. . . . . . 7
⊢ (((𝑥 ∈ N ∧
𝑦 ∈ N)
∧ (𝑧 ∈ ω
∧ 𝑤 ∈
N)) → [〈((𝑥 ·𝑜 𝑤) +𝑜 (𝑦 ·𝑜
𝑧)), (𝑦 ·𝑜 𝑤)〉]
~Q ∈ Q) |
43 | | nqnq0pi 6536 |
. . . . . . . . 9
⊢ ((((𝑥 ·𝑜
𝑤) +𝑜
(𝑦
·𝑜 𝑧)) ∈ N ∧ (𝑦 ·𝑜
𝑤) ∈ N)
→ [〈((𝑥
·𝑜 𝑤) +𝑜 (𝑦 ·𝑜 𝑧)), (𝑦 ·𝑜 𝑤)〉]
~Q0 = [〈((𝑥 ·𝑜 𝑤) +𝑜 (𝑦 ·𝑜
𝑧)), (𝑦 ·𝑜 𝑤)〉]
~Q ) |
44 | 43 | eleq1d 2106 |
. . . . . . . 8
⊢ ((((𝑥 ·𝑜
𝑤) +𝑜
(𝑦
·𝑜 𝑧)) ∈ N ∧ (𝑦 ·𝑜
𝑤) ∈ N)
→ ([〈((𝑥
·𝑜 𝑤) +𝑜 (𝑦 ·𝑜 𝑧)), (𝑦 ·𝑜 𝑤)〉]
~Q0 ∈ Q ↔ [〈((𝑥 ·𝑜
𝑤) +𝑜
(𝑦
·𝑜 𝑧)), (𝑦 ·𝑜 𝑤)〉]
~Q ∈ Q)) |
45 | 31, 35, 44 | syl2anc 391 |
. . . . . . 7
⊢ (((𝑥 ∈ N ∧
𝑦 ∈ N)
∧ (𝑧 ∈ ω
∧ 𝑤 ∈
N)) → ([〈((𝑥 ·𝑜 𝑤) +𝑜 (𝑦 ·𝑜
𝑧)), (𝑦 ·𝑜 𝑤)〉]
~Q0 ∈ Q ↔ [〈((𝑥 ·𝑜
𝑤) +𝑜
(𝑦
·𝑜 𝑧)), (𝑦 ·𝑜 𝑤)〉]
~Q ∈ Q)) |
46 | 42, 45 | mpbird 156 |
. . . . . 6
⊢ (((𝑥 ∈ N ∧
𝑦 ∈ N)
∧ (𝑧 ∈ ω
∧ 𝑤 ∈
N)) → [〈((𝑥 ·𝑜 𝑤) +𝑜 (𝑦 ·𝑜
𝑧)), (𝑦 ·𝑜 𝑤)〉]
~Q0 ∈ Q) |
47 | 46 | ad2ant2r 478 |
. . . . 5
⊢ ((((𝑥 ∈ N ∧
𝑦 ∈ N)
∧ 𝐴 = [〈𝑥, 𝑦〉] ~Q ) ∧
((𝑧 ∈ ω ∧
𝑤 ∈ N)
∧ 𝐵 = [〈𝑧, 𝑤〉] ~Q0 ))
→ [〈((𝑥
·𝑜 𝑤) +𝑜 (𝑦 ·𝑜 𝑧)), (𝑦 ·𝑜 𝑤)〉]
~Q0 ∈ Q) |
48 | 16, 47 | eqeltrd 2114 |
. . . 4
⊢ ((((𝑥 ∈ N ∧
𝑦 ∈ N)
∧ 𝐴 = [〈𝑥, 𝑦〉] ~Q ) ∧
((𝑧 ∈ ω ∧
𝑤 ∈ N)
∧ 𝐵 = [〈𝑧, 𝑤〉] ~Q0 ))
→ (𝐴
+Q0 𝐵) ∈ Q) |
49 | 48 | exlimivv 1776 |
. . 3
⊢
(∃𝑧∃𝑤(((𝑥 ∈ N ∧ 𝑦 ∈ N) ∧
𝐴 = [〈𝑥, 𝑦〉] ~Q ) ∧
((𝑧 ∈ ω ∧
𝑤 ∈ N)
∧ 𝐵 = [〈𝑧, 𝑤〉] ~Q0 ))
→ (𝐴
+Q0 𝐵) ∈ Q) |
50 | 49 | exlimivv 1776 |
. 2
⊢
(∃𝑥∃𝑦∃𝑧∃𝑤(((𝑥 ∈ N ∧ 𝑦 ∈ N) ∧
𝐴 = [〈𝑥, 𝑦〉] ~Q ) ∧
((𝑧 ∈ ω ∧
𝑤 ∈ N)
∧ 𝐵 = [〈𝑧, 𝑤〉] ~Q0 ))
→ (𝐴
+Q0 𝐵) ∈ Q) |
51 | 5, 50 | syl 14 |
1
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈
Q0) → (𝐴 +Q0 𝐵) ∈
Q) |