Proof of Theorem adderpq
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nqercl 10972 | . . . 4
⊢ (𝐴 ∈ (N ×
N) → ([Q]‘𝐴) ∈ Q) | 
| 2 |  | nqercl 10972 | . . . 4
⊢ (𝐵 ∈ (N ×
N) → ([Q]‘𝐵) ∈ Q) | 
| 3 |  | addpqnq 10979 | . . . 4
⊢
((([Q]‘𝐴) ∈ Q ∧
([Q]‘𝐵)
∈ Q) → (([Q]‘𝐴) +Q
([Q]‘𝐵)) =
([Q]‘(([Q]‘𝐴) +pQ
([Q]‘𝐵)))) | 
| 4 | 1, 2, 3 | syl2an 596 | . . 3
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) →
(([Q]‘𝐴) +Q
([Q]‘𝐵)) =
([Q]‘(([Q]‘𝐴) +pQ
([Q]‘𝐵)))) | 
| 5 |  | enqer 10962 | . . . . . 6
⊢ 
~Q Er (N ×
N) | 
| 6 | 5 | a1i 11 | . . . . 5
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) →
~Q Er (N ×
N)) | 
| 7 |  | nqerrel 10973 | . . . . . . 7
⊢ (𝐴 ∈ (N ×
N) → 𝐴
~Q ([Q]‘𝐴)) | 
| 8 | 7 | adantr 480 | . . . . . 6
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) → 𝐴 ~Q
([Q]‘𝐴)) | 
| 9 |  | elpqn 10966 | . . . . . . . . 9
⊢
(([Q]‘𝐴) ∈ Q →
([Q]‘𝐴)
∈ (N × N)) | 
| 10 | 1, 9 | syl 17 | . . . . . . . 8
⊢ (𝐴 ∈ (N ×
N) → ([Q]‘𝐴) ∈ (N ×
N)) | 
| 11 |  | adderpqlem 10995 | . . . . . . . . 9
⊢ ((𝐴 ∈ (N ×
N) ∧ ([Q]‘𝐴) ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) → (𝐴 ~Q
([Q]‘𝐴)
↔ (𝐴
+pQ 𝐵) ~Q
(([Q]‘𝐴) +pQ 𝐵))) | 
| 12 | 11 | 3exp 1119 | . . . . . . . 8
⊢ (𝐴 ∈ (N ×
N) → (([Q]‘𝐴) ∈ (N ×
N) → (𝐵
∈ (N × N) → (𝐴 ~Q
([Q]‘𝐴)
↔ (𝐴
+pQ 𝐵) ~Q
(([Q]‘𝐴) +pQ 𝐵))))) | 
| 13 | 10, 12 | mpd 15 | . . . . . . 7
⊢ (𝐴 ∈ (N ×
N) → (𝐵
∈ (N × N) → (𝐴 ~Q
([Q]‘𝐴)
↔ (𝐴
+pQ 𝐵) ~Q
(([Q]‘𝐴) +pQ 𝐵)))) | 
| 14 | 13 | imp 406 | . . . . . 6
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) → (𝐴 ~Q
([Q]‘𝐴)
↔ (𝐴
+pQ 𝐵) ~Q
(([Q]‘𝐴) +pQ 𝐵))) | 
| 15 | 8, 14 | mpbid 232 | . . . . 5
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) → (𝐴 +pQ 𝐵) ~Q
(([Q]‘𝐴) +pQ 𝐵)) | 
| 16 |  | nqerrel 10973 | . . . . . . . 8
⊢ (𝐵 ∈ (N ×
N) → 𝐵
~Q ([Q]‘𝐵)) | 
| 17 | 16 | adantl 481 | . . . . . . 7
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) → 𝐵 ~Q
([Q]‘𝐵)) | 
| 18 |  | elpqn 10966 | . . . . . . . . . 10
⊢
(([Q]‘𝐵) ∈ Q →
([Q]‘𝐵)
∈ (N × N)) | 
| 19 | 2, 18 | syl 17 | . . . . . . . . 9
⊢ (𝐵 ∈ (N ×
N) → ([Q]‘𝐵) ∈ (N ×
N)) | 
| 20 |  | adderpqlem 10995 | . . . . . . . . . 10
⊢ ((𝐵 ∈ (N ×
N) ∧ ([Q]‘𝐵) ∈ (N ×
N) ∧ ([Q]‘𝐴) ∈ (N ×
N)) → (𝐵
~Q ([Q]‘𝐵) ↔ (𝐵 +pQ
([Q]‘𝐴)) ~Q
(([Q]‘𝐵) +pQ
([Q]‘𝐴)))) | 
| 21 | 20 | 3exp 1119 | . . . . . . . . 9
⊢ (𝐵 ∈ (N ×
N) → (([Q]‘𝐵) ∈ (N ×
N) → (([Q]‘𝐴) ∈ (N ×
N) → (𝐵
~Q ([Q]‘𝐵) ↔ (𝐵 +pQ
([Q]‘𝐴)) ~Q
(([Q]‘𝐵) +pQ
([Q]‘𝐴)))))) | 
| 22 | 19, 21 | mpd 15 | . . . . . . . 8
⊢ (𝐵 ∈ (N ×
N) → (([Q]‘𝐴) ∈ (N ×
N) → (𝐵
~Q ([Q]‘𝐵) ↔ (𝐵 +pQ
([Q]‘𝐴)) ~Q
(([Q]‘𝐵) +pQ
([Q]‘𝐴))))) | 
| 23 | 10, 22 | mpan9 506 | . . . . . . 7
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) → (𝐵 ~Q
([Q]‘𝐵)
↔ (𝐵
+pQ ([Q]‘𝐴)) ~Q
(([Q]‘𝐵) +pQ
([Q]‘𝐴)))) | 
| 24 | 17, 23 | mpbid 232 | . . . . . 6
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) → (𝐵 +pQ
([Q]‘𝐴)) ~Q
(([Q]‘𝐵) +pQ
([Q]‘𝐴))) | 
| 25 |  | addcompq 10991 | . . . . . 6
⊢ (𝐵 +pQ
([Q]‘𝐴)) = (([Q]‘𝐴) +pQ
𝐵) | 
| 26 |  | addcompq 10991 | . . . . . 6
⊢
(([Q]‘𝐵) +pQ
([Q]‘𝐴)) = (([Q]‘𝐴) +pQ
([Q]‘𝐵)) | 
| 27 | 24, 25, 26 | 3brtr3g 5175 | . . . . 5
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) →
(([Q]‘𝐴) +pQ 𝐵) ~Q
(([Q]‘𝐴) +pQ
([Q]‘𝐵))) | 
| 28 | 6, 15, 27 | ertrd 8762 | . . . 4
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) → (𝐴 +pQ 𝐵) ~Q
(([Q]‘𝐴) +pQ
([Q]‘𝐵))) | 
| 29 |  | addpqf 10985 | . . . . . 6
⊢ 
+pQ :((N × N)
× (N × N))⟶(N
× N) | 
| 30 | 29 | fovcl 7562 | . . . . 5
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) → (𝐴 +pQ 𝐵) ∈ (N
× N)) | 
| 31 | 29 | fovcl 7562 | . . . . . 6
⊢
((([Q]‘𝐴) ∈ (N ×
N) ∧ ([Q]‘𝐵) ∈ (N ×
N)) → (([Q]‘𝐴) +pQ
([Q]‘𝐵)) ∈ (N ×
N)) | 
| 32 | 10, 19, 31 | syl2an 596 | . . . . 5
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) →
(([Q]‘𝐴) +pQ
([Q]‘𝐵)) ∈ (N ×
N)) | 
| 33 |  | nqereq 10976 | . . . . 5
⊢ (((𝐴 +pQ
𝐵) ∈ (N
× N) ∧ (([Q]‘𝐴) +pQ
([Q]‘𝐵)) ∈ (N ×
N)) → ((𝐴 +pQ 𝐵) ~Q
(([Q]‘𝐴) +pQ
([Q]‘𝐵)) ↔ ([Q]‘(𝐴 +pQ
𝐵)) =
([Q]‘(([Q]‘𝐴) +pQ
([Q]‘𝐵))))) | 
| 34 | 30, 32, 33 | syl2anc 584 | . . . 4
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) → ((𝐴 +pQ 𝐵) ~Q
(([Q]‘𝐴) +pQ
([Q]‘𝐵)) ↔ ([Q]‘(𝐴 +pQ
𝐵)) =
([Q]‘(([Q]‘𝐴) +pQ
([Q]‘𝐵))))) | 
| 35 | 28, 34 | mpbid 232 | . . 3
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) →
([Q]‘(𝐴
+pQ 𝐵)) =
([Q]‘(([Q]‘𝐴) +pQ
([Q]‘𝐵)))) | 
| 36 | 4, 35 | eqtr4d 2779 | . 2
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) →
(([Q]‘𝐴) +Q
([Q]‘𝐵)) = ([Q]‘(𝐴 +pQ
𝐵))) | 
| 37 |  | 0nnq 10965 | . . . . . . 7
⊢  ¬
∅ ∈ Q | 
| 38 |  | nqerf 10971 | . . . . . . . . . . 11
⊢
[Q]:(N ×
N)⟶Q | 
| 39 | 38 | fdmi 6746 | . . . . . . . . . 10
⊢ dom
[Q] = (N × N) | 
| 40 | 39 | eleq2i 2832 | . . . . . . . . 9
⊢ (𝐴 ∈ dom [Q]
↔ 𝐴 ∈
(N × N)) | 
| 41 |  | ndmfv 6940 | . . . . . . . . 9
⊢ (¬
𝐴 ∈ dom
[Q] → ([Q]‘𝐴) = ∅) | 
| 42 | 40, 41 | sylnbir 331 | . . . . . . . 8
⊢ (¬
𝐴 ∈ (N
× N) → ([Q]‘𝐴) = ∅) | 
| 43 | 42 | eleq1d 2825 | . . . . . . 7
⊢ (¬
𝐴 ∈ (N
× N) → (([Q]‘𝐴) ∈ Q ↔ ∅
∈ Q)) | 
| 44 | 37, 43 | mtbiri 327 | . . . . . 6
⊢ (¬
𝐴 ∈ (N
× N) → ¬ ([Q]‘𝐴) ∈
Q) | 
| 45 | 44 | con4i 114 | . . . . 5
⊢
(([Q]‘𝐴) ∈ Q → 𝐴 ∈ (N ×
N)) | 
| 46 | 39 | eleq2i 2832 | . . . . . . . . 9
⊢ (𝐵 ∈ dom [Q]
↔ 𝐵 ∈
(N × N)) | 
| 47 |  | ndmfv 6940 | . . . . . . . . 9
⊢ (¬
𝐵 ∈ dom
[Q] → ([Q]‘𝐵) = ∅) | 
| 48 | 46, 47 | sylnbir 331 | . . . . . . . 8
⊢ (¬
𝐵 ∈ (N
× N) → ([Q]‘𝐵) = ∅) | 
| 49 | 48 | eleq1d 2825 | . . . . . . 7
⊢ (¬
𝐵 ∈ (N
× N) → (([Q]‘𝐵) ∈ Q ↔ ∅
∈ Q)) | 
| 50 | 37, 49 | mtbiri 327 | . . . . . 6
⊢ (¬
𝐵 ∈ (N
× N) → ¬ ([Q]‘𝐵) ∈
Q) | 
| 51 | 50 | con4i 114 | . . . . 5
⊢
(([Q]‘𝐵) ∈ Q → 𝐵 ∈ (N ×
N)) | 
| 52 | 45, 51 | anim12i 613 | . . . 4
⊢
((([Q]‘𝐴) ∈ Q ∧
([Q]‘𝐵)
∈ Q) → (𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N))) | 
| 53 |  | addnqf 10989 | . . . . . 6
⊢ 
+Q :(Q ×
Q)⟶Q | 
| 54 | 53 | fdmi 6746 | . . . . 5
⊢ dom
+Q = (Q ×
Q) | 
| 55 | 54 | ndmov 7618 | . . . 4
⊢ (¬
(([Q]‘𝐴) ∈ Q ∧
([Q]‘𝐵)
∈ Q) → (([Q]‘𝐴) +Q
([Q]‘𝐵)) = ∅) | 
| 56 | 52, 55 | nsyl5 159 | . . 3
⊢ (¬
(𝐴 ∈ (N
× N) ∧ 𝐵 ∈ (N ×
N)) → (([Q]‘𝐴) +Q
([Q]‘𝐵)) = ∅) | 
| 57 |  | 0nelxp 5718 | . . . . . 6
⊢  ¬
∅ ∈ (N × N) | 
| 58 | 39 | eleq2i 2832 | . . . . . 6
⊢ (∅
∈ dom [Q] ↔ ∅ ∈ (N ×
N)) | 
| 59 | 57, 58 | mtbir 323 | . . . . 5
⊢  ¬
∅ ∈ dom [Q] | 
| 60 | 29 | fdmi 6746 | . . . . . . 7
⊢ dom
+pQ = ((N × N)
× (N × N)) | 
| 61 | 60 | ndmov 7618 | . . . . . 6
⊢ (¬
(𝐴 ∈ (N
× N) ∧ 𝐵 ∈ (N ×
N)) → (𝐴
+pQ 𝐵) = ∅) | 
| 62 | 61 | eleq1d 2825 | . . . . 5
⊢ (¬
(𝐴 ∈ (N
× N) ∧ 𝐵 ∈ (N ×
N)) → ((𝐴 +pQ 𝐵) ∈ dom [Q]
↔ ∅ ∈ dom [Q])) | 
| 63 | 59, 62 | mtbiri 327 | . . . 4
⊢ (¬
(𝐴 ∈ (N
× N) ∧ 𝐵 ∈ (N ×
N)) → ¬ (𝐴 +pQ 𝐵) ∈ dom
[Q]) | 
| 64 |  | ndmfv 6940 | . . . 4
⊢ (¬
(𝐴
+pQ 𝐵) ∈ dom [Q] →
([Q]‘(𝐴
+pQ 𝐵)) = ∅) | 
| 65 | 63, 64 | syl 17 | . . 3
⊢ (¬
(𝐴 ∈ (N
× N) ∧ 𝐵 ∈ (N ×
N)) → ([Q]‘(𝐴 +pQ 𝐵)) = ∅) | 
| 66 | 56, 65 | eqtr4d 2779 | . 2
⊢ (¬
(𝐴 ∈ (N
× N) ∧ 𝐵 ∈ (N ×
N)) → (([Q]‘𝐴) +Q
([Q]‘𝐵)) = ([Q]‘(𝐴 +pQ
𝐵))) | 
| 67 | 36, 66 | pm2.61i 182 | 1
⊢
(([Q]‘𝐴) +Q
([Q]‘𝐵)) = ([Q]‘(𝐴 +pQ
𝐵)) |