Step | Hyp | Ref
| Expression |
1 | | nqpi 7340 |
. . . 4
⊢ (𝐴 ∈ Q →
∃𝑧∃𝑤((𝑧 ∈ N ∧ 𝑤 ∈ N) ∧
𝐴 = [〈𝑧, 𝑤〉] ~Q
)) |
2 | | nqpi 7340 |
. . . 4
⊢ (𝐵 ∈ Q →
∃𝑣∃𝑢((𝑣 ∈ N ∧ 𝑢 ∈ N) ∧
𝐵 = [〈𝑣, 𝑢〉] ~Q
)) |
3 | 1, 2 | anim12i 336 |
. . 3
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (∃𝑧∃𝑤((𝑧 ∈ N ∧ 𝑤 ∈ N) ∧
𝐴 = [〈𝑧, 𝑤〉] ~Q ) ∧
∃𝑣∃𝑢((𝑣 ∈ N ∧ 𝑢 ∈ N) ∧
𝐵 = [〈𝑣, 𝑢〉] ~Q
))) |
4 | | ee4anv 1927 |
. . 3
⊢
(∃𝑧∃𝑤∃𝑣∃𝑢(((𝑧 ∈ N ∧ 𝑤 ∈ N) ∧
𝐴 = [〈𝑧, 𝑤〉] ~Q ) ∧
((𝑣 ∈ N
∧ 𝑢 ∈
N) ∧ 𝐵 =
[〈𝑣, 𝑢〉]
~Q )) ↔ (∃𝑧∃𝑤((𝑧 ∈ N ∧ 𝑤 ∈ N) ∧
𝐴 = [〈𝑧, 𝑤〉] ~Q ) ∧
∃𝑣∃𝑢((𝑣 ∈ N ∧ 𝑢 ∈ N) ∧
𝐵 = [〈𝑣, 𝑢〉] ~Q
))) |
5 | 3, 4 | sylibr 133 |
. 2
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ∃𝑧∃𝑤∃𝑣∃𝑢(((𝑧 ∈ N ∧ 𝑤 ∈ N) ∧
𝐴 = [〈𝑧, 𝑤〉] ~Q ) ∧
((𝑣 ∈ N
∧ 𝑢 ∈
N) ∧ 𝐵 =
[〈𝑣, 𝑢〉]
~Q ))) |
6 | | oveq12 5862 |
. . . . . . 7
⊢ ((𝐴 = [〈𝑧, 𝑤〉] ~Q ∧
𝐵 = [〈𝑣, 𝑢〉] ~Q ) →
(𝐴
+Q 𝐵) = ([〈𝑧, 𝑤〉] ~Q
+Q [〈𝑣, 𝑢〉] ~Q
)) |
7 | | mulclpi 7290 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ N ∧
𝑢 ∈ N)
→ (𝑧
·N 𝑢) ∈ N) |
8 | 7 | ad2ant2rl 508 |
. . . . . . . . . . . 12
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → (𝑧 ·N 𝑢) ∈
N) |
9 | | mulclpi 7290 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ N ∧
𝑣 ∈ N)
→ (𝑤
·N 𝑣) ∈ N) |
10 | 9 | ad2ant2lr 507 |
. . . . . . . . . . . 12
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → (𝑤 ·N 𝑣) ∈
N) |
11 | | addpiord 7278 |
. . . . . . . . . . . 12
⊢ (((𝑧
·N 𝑢) ∈ N ∧ (𝑤
·N 𝑣) ∈ N) → ((𝑧
·N 𝑢) +N (𝑤
·N 𝑣)) = ((𝑧 ·N 𝑢) +o (𝑤
·N 𝑣))) |
12 | 8, 10, 11 | syl2anc 409 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → ((𝑧 ·N 𝑢) +N
(𝑤
·N 𝑣)) = ((𝑧 ·N 𝑢) +o (𝑤
·N 𝑣))) |
13 | | mulpiord 7279 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ N ∧
𝑢 ∈ N)
→ (𝑧
·N 𝑢) = (𝑧 ·o 𝑢)) |
14 | 13 | ad2ant2rl 508 |
. . . . . . . . . . . 12
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → (𝑧 ·N 𝑢) = (𝑧 ·o 𝑢)) |
15 | | mulpiord 7279 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ N ∧
𝑣 ∈ N)
→ (𝑤
·N 𝑣) = (𝑤 ·o 𝑣)) |
16 | 15 | ad2ant2lr 507 |
. . . . . . . . . . . 12
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → (𝑤 ·N 𝑣) = (𝑤 ·o 𝑣)) |
17 | 14, 16 | oveq12d 5871 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → ((𝑧 ·N 𝑢) +o (𝑤
·N 𝑣)) = ((𝑧 ·o 𝑢) +o (𝑤 ·o 𝑣))) |
18 | 12, 17 | eqtrd 2203 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → ((𝑧 ·N 𝑢) +N
(𝑤
·N 𝑣)) = ((𝑧 ·o 𝑢) +o (𝑤 ·o 𝑣))) |
19 | | mulpiord 7279 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ N ∧
𝑢 ∈ N)
→ (𝑤
·N 𝑢) = (𝑤 ·o 𝑢)) |
20 | 19 | ad2ant2l 505 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → (𝑤 ·N 𝑢) = (𝑤 ·o 𝑢)) |
21 | 18, 20 | opeq12d 3773 |
. . . . . . . . 9
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → 〈((𝑧 ·N 𝑢) +N
(𝑤
·N 𝑣)), (𝑤 ·N 𝑢)〉 = 〈((𝑧 ·o 𝑢) +o (𝑤 ·o 𝑣)), (𝑤 ·o 𝑢)〉) |
22 | 21 | eceq1d 6549 |
. . . . . . . 8
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → [〈((𝑧 ·N 𝑢) +N
(𝑤
·N 𝑣)), (𝑤 ·N 𝑢)〉]
~Q0 = [〈((𝑧 ·o 𝑢) +o (𝑤 ·o 𝑣)), (𝑤 ·o 𝑢)〉] ~Q0
) |
23 | | addpipqqs 7332 |
. . . . . . . . 9
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → ([〈𝑧, 𝑤〉] ~Q
+Q [〈𝑣, 𝑢〉] ~Q ) =
[〈((𝑧
·N 𝑢) +N (𝑤
·N 𝑣)), (𝑤 ·N 𝑢)〉]
~Q ) |
24 | | addclpi 7289 |
. . . . . . . . . . 11
⊢ (((𝑧
·N 𝑢) ∈ N ∧ (𝑤
·N 𝑣) ∈ N) → ((𝑧
·N 𝑢) +N (𝑤
·N 𝑣)) ∈ N) |
25 | 8, 10, 24 | syl2anc 409 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → ((𝑧 ·N 𝑢) +N
(𝑤
·N 𝑣)) ∈ N) |
26 | | mulclpi 7290 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ N ∧
𝑢 ∈ N)
→ (𝑤
·N 𝑢) ∈ N) |
27 | 26 | ad2ant2l 505 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → (𝑤 ·N 𝑢) ∈
N) |
28 | | nqnq0pi 7400 |
. . . . . . . . . 10
⊢ ((((𝑧
·N 𝑢) +N (𝑤
·N 𝑣)) ∈ N ∧ (𝑤
·N 𝑢) ∈ N) →
[〈((𝑧
·N 𝑢) +N (𝑤
·N 𝑣)), (𝑤 ·N 𝑢)〉]
~Q0 = [〈((𝑧 ·N 𝑢) +N
(𝑤
·N 𝑣)), (𝑤 ·N 𝑢)〉]
~Q ) |
29 | 25, 27, 28 | syl2anc 409 |
. . . . . . . . 9
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → [〈((𝑧 ·N 𝑢) +N
(𝑤
·N 𝑣)), (𝑤 ·N 𝑢)〉]
~Q0 = [〈((𝑧 ·N 𝑢) +N
(𝑤
·N 𝑣)), (𝑤 ·N 𝑢)〉]
~Q ) |
30 | 23, 29 | eqtr4d 2206 |
. . . . . . . 8
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → ([〈𝑧, 𝑤〉] ~Q
+Q [〈𝑣, 𝑢〉] ~Q ) =
[〈((𝑧
·N 𝑢) +N (𝑤
·N 𝑣)), (𝑤 ·N 𝑢)〉]
~Q0 ) |
31 | | pinn 7271 |
. . . . . . . . . 10
⊢ (𝑧 ∈ N →
𝑧 ∈
ω) |
32 | 31 | anim1i 338 |
. . . . . . . . 9
⊢ ((𝑧 ∈ N ∧
𝑤 ∈ N)
→ (𝑧 ∈ ω
∧ 𝑤 ∈
N)) |
33 | | pinn 7271 |
. . . . . . . . . 10
⊢ (𝑣 ∈ N →
𝑣 ∈
ω) |
34 | 33 | anim1i 338 |
. . . . . . . . 9
⊢ ((𝑣 ∈ N ∧
𝑢 ∈ N)
→ (𝑣 ∈ ω
∧ 𝑢 ∈
N)) |
35 | | addnnnq0 7411 |
. . . . . . . . 9
⊢ (((𝑧 ∈ ω ∧ 𝑤 ∈ N) ∧
(𝑣 ∈ ω ∧
𝑢 ∈ N))
→ ([〈𝑧, 𝑤〉]
~Q0 +Q0 [〈𝑣, 𝑢〉] ~Q0 ) =
[〈((𝑧
·o 𝑢)
+o (𝑤
·o 𝑣)),
(𝑤 ·o
𝑢)〉]
~Q0 ) |
36 | 32, 34, 35 | syl2an 287 |
. . . . . . . 8
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → ([〈𝑧, 𝑤〉] ~Q0
+Q0 [〈𝑣, 𝑢〉] ~Q0 ) =
[〈((𝑧
·o 𝑢)
+o (𝑤
·o 𝑣)),
(𝑤 ·o
𝑢)〉]
~Q0 ) |
37 | 22, 30, 36 | 3eqtr4d 2213 |
. . . . . . 7
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → ([〈𝑧, 𝑤〉] ~Q
+Q [〈𝑣, 𝑢〉] ~Q ) =
([〈𝑧, 𝑤〉]
~Q0 +Q0 [〈𝑣, 𝑢〉] ~Q0
)) |
38 | 6, 37 | sylan9eqr 2225 |
. . . . . 6
⊢ ((((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) ∧ (𝐴 = [〈𝑧, 𝑤〉] ~Q ∧
𝐵 = [〈𝑣, 𝑢〉] ~Q )) →
(𝐴
+Q 𝐵) = ([〈𝑧, 𝑤〉] ~Q0
+Q0 [〈𝑣, 𝑢〉] ~Q0
)) |
39 | | nqnq0pi 7400 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ N ∧
𝑤 ∈ N)
→ [〈𝑧, 𝑤〉]
~Q0 = [〈𝑧, 𝑤〉] ~Q
) |
40 | 39 | adantr 274 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → [〈𝑧, 𝑤〉] ~Q0 =
[〈𝑧, 𝑤〉]
~Q ) |
41 | 40 | eqeq2d 2182 |
. . . . . . . . 9
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → (𝐴 = [〈𝑧, 𝑤〉] ~Q0 ↔
𝐴 = [〈𝑧, 𝑤〉] ~Q
)) |
42 | | nqnq0pi 7400 |
. . . . . . . . . . 11
⊢ ((𝑣 ∈ N ∧
𝑢 ∈ N)
→ [〈𝑣, 𝑢〉]
~Q0 = [〈𝑣, 𝑢〉] ~Q
) |
43 | 42 | adantl 275 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → [〈𝑣, 𝑢〉] ~Q0 =
[〈𝑣, 𝑢〉]
~Q ) |
44 | 43 | eqeq2d 2182 |
. . . . . . . . 9
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → (𝐵 = [〈𝑣, 𝑢〉] ~Q0 ↔
𝐵 = [〈𝑣, 𝑢〉] ~Q
)) |
45 | 41, 44 | anbi12d 470 |
. . . . . . . 8
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → ((𝐴 = [〈𝑧, 𝑤〉] ~Q0 ∧
𝐵 = [〈𝑣, 𝑢〉] ~Q0 ) ↔
(𝐴 = [〈𝑧, 𝑤〉] ~Q ∧
𝐵 = [〈𝑣, 𝑢〉] ~Q
))) |
46 | 45 | pm5.32i 451 |
. . . . . . 7
⊢ ((((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) ∧ (𝐴 = [〈𝑧, 𝑤〉] ~Q0 ∧
𝐵 = [〈𝑣, 𝑢〉] ~Q0 ))
↔ (((𝑧 ∈
N ∧ 𝑤
∈ N) ∧ (𝑣 ∈ N ∧ 𝑢 ∈ N)) ∧
(𝐴 = [〈𝑧, 𝑤〉] ~Q ∧
𝐵 = [〈𝑣, 𝑢〉] ~Q
))) |
47 | | oveq12 5862 |
. . . . . . . 8
⊢ ((𝐴 = [〈𝑧, 𝑤〉] ~Q0 ∧
𝐵 = [〈𝑣, 𝑢〉] ~Q0 ) →
(𝐴
+Q0 𝐵) = ([〈𝑧, 𝑤〉] ~Q0
+Q0 [〈𝑣, 𝑢〉] ~Q0
)) |
48 | 47 | adantl 275 |
. . . . . . 7
⊢ ((((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) ∧ (𝐴 = [〈𝑧, 𝑤〉] ~Q0 ∧
𝐵 = [〈𝑣, 𝑢〉] ~Q0 ))
→ (𝐴
+Q0 𝐵) = ([〈𝑧, 𝑤〉] ~Q0
+Q0 [〈𝑣, 𝑢〉] ~Q0
)) |
49 | 46, 48 | sylbir 134 |
. . . . . 6
⊢ ((((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) ∧ (𝐴 = [〈𝑧, 𝑤〉] ~Q ∧
𝐵 = [〈𝑣, 𝑢〉] ~Q )) →
(𝐴
+Q0 𝐵) = ([〈𝑧, 𝑤〉] ~Q0
+Q0 [〈𝑣, 𝑢〉] ~Q0
)) |
50 | 38, 49 | eqtr4d 2206 |
. . . . 5
⊢ ((((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) ∧ (𝐴 = [〈𝑧, 𝑤〉] ~Q ∧
𝐵 = [〈𝑣, 𝑢〉] ~Q )) →
(𝐴
+Q 𝐵) = (𝐴 +Q0 𝐵)) |
51 | 50 | an4s 583 |
. . . 4
⊢ ((((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ 𝐴 = [〈𝑧, 𝑤〉] ~Q ) ∧
((𝑣 ∈ N
∧ 𝑢 ∈
N) ∧ 𝐵 =
[〈𝑣, 𝑢〉]
~Q )) → (𝐴 +Q 𝐵) = (𝐴 +Q0 𝐵)) |
52 | 51 | exlimivv 1889 |
. . 3
⊢
(∃𝑣∃𝑢(((𝑧 ∈ N ∧ 𝑤 ∈ N) ∧
𝐴 = [〈𝑧, 𝑤〉] ~Q ) ∧
((𝑣 ∈ N
∧ 𝑢 ∈
N) ∧ 𝐵 =
[〈𝑣, 𝑢〉]
~Q )) → (𝐴 +Q 𝐵) = (𝐴 +Q0 𝐵)) |
53 | 52 | exlimivv 1889 |
. 2
⊢
(∃𝑧∃𝑤∃𝑣∃𝑢(((𝑧 ∈ N ∧ 𝑤 ∈ N) ∧
𝐴 = [〈𝑧, 𝑤〉] ~Q ) ∧
((𝑣 ∈ N
∧ 𝑢 ∈
N) ∧ 𝐵 =
[〈𝑣, 𝑢〉]
~Q )) → (𝐴 +Q 𝐵) = (𝐴 +Q0 𝐵)) |
54 | 5, 53 | syl 14 |
1
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (𝐴
+Q 𝐵) = (𝐴 +Q0 𝐵)) |