Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  addclnq GIF version

 Description: Closure of addition on positive fractions. (Contributed by NM, 29-Aug-1995.)
Assertion
Ref Expression
addclnq ((𝐴Q𝐵Q) → (𝐴 +Q 𝐵) ∈ Q)

Dummy variables 𝑥 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-nqqs 6403 . . 3 Q = ((N × N) / ~Q )
2 oveq1 5482 . . . 4 ([⟨𝑥, 𝑦⟩] ~Q = 𝐴 → ([⟨𝑥, 𝑦⟩] ~Q +Q [⟨𝑧, 𝑤⟩] ~Q ) = (𝐴 +Q [⟨𝑧, 𝑤⟩] ~Q ))
32eleq1d 2106 . . 3 ([⟨𝑥, 𝑦⟩] ~Q = 𝐴 → (([⟨𝑥, 𝑦⟩] ~Q +Q [⟨𝑧, 𝑤⟩] ~Q ) ∈ ((N × N) / ~Q ) ↔ (𝐴 +Q [⟨𝑧, 𝑤⟩] ~Q ) ∈ ((N × N) / ~Q )))
4 oveq2 5483 . . . 4 ([⟨𝑧, 𝑤⟩] ~Q = 𝐵 → (𝐴 +Q [⟨𝑧, 𝑤⟩] ~Q ) = (𝐴 +Q 𝐵))
54eleq1d 2106 . . 3 ([⟨𝑧, 𝑤⟩] ~Q = 𝐵 → ((𝐴 +Q [⟨𝑧, 𝑤⟩] ~Q ) ∈ ((N × N) / ~Q ) ↔ (𝐴 +Q 𝐵) ∈ ((N × N) / ~Q )))
6 addpipqqs 6425 . . . 4 (((𝑥N𝑦N) ∧ (𝑧N𝑤N)) → ([⟨𝑥, 𝑦⟩] ~Q +Q [⟨𝑧, 𝑤⟩] ~Q ) = [⟨((𝑥 ·N 𝑤) +N (𝑦 ·N 𝑧)), (𝑦 ·N 𝑤)⟩] ~Q )
7 mulclpi 6383 . . . . . . . 8 ((𝑥N𝑤N) → (𝑥 ·N 𝑤) ∈ N)
8 mulclpi 6383 . . . . . . . 8 ((𝑦N𝑧N) → (𝑦 ·N 𝑧) ∈ N)
9 addclpi 6382 . . . . . . . 8 (((𝑥 ·N 𝑤) ∈ N ∧ (𝑦 ·N 𝑧) ∈ N) → ((𝑥 ·N 𝑤) +N (𝑦 ·N 𝑧)) ∈ N)
107, 8, 9syl2an 273 . . . . . . 7 (((𝑥N𝑤N) ∧ (𝑦N𝑧N)) → ((𝑥 ·N 𝑤) +N (𝑦 ·N 𝑧)) ∈ N)
1110an42s 523 . . . . . 6 (((𝑥N𝑦N) ∧ (𝑧N𝑤N)) → ((𝑥 ·N 𝑤) +N (𝑦 ·N 𝑧)) ∈ N)
12 mulclpi 6383 . . . . . . 7 ((𝑦N𝑤N) → (𝑦 ·N 𝑤) ∈ N)
1312ad2ant2l 477 . . . . . 6 (((𝑥N𝑦N) ∧ (𝑧N𝑤N)) → (𝑦 ·N 𝑤) ∈ N)
1411, 13jca 290 . . . . 5 (((𝑥N𝑦N) ∧ (𝑧N𝑤N)) → (((𝑥 ·N 𝑤) +N (𝑦 ·N 𝑧)) ∈ N ∧ (𝑦 ·N 𝑤) ∈ N))
15 opelxpi 4339 . . . . 5 ((((𝑥 ·N 𝑤) +N (𝑦 ·N 𝑧)) ∈ N ∧ (𝑦 ·N 𝑤) ∈ N) → ⟨((𝑥 ·N 𝑤) +N (𝑦 ·N 𝑧)), (𝑦 ·N 𝑤)⟩ ∈ (N × N))
16 enqex 6415 . . . . . 6 ~Q ∈ V
1716ecelqsi 6123 . . . . 5 (⟨((𝑥 ·N 𝑤) +N (𝑦 ·N 𝑧)), (𝑦 ·N 𝑤)⟩ ∈ (N × N) → [⟨((𝑥 ·N 𝑤) +N (𝑦 ·N 𝑧)), (𝑦 ·N 𝑤)⟩] ~Q ∈ ((N × N) / ~Q ))
1814, 15, 173syl 17 . . . 4 (((𝑥N𝑦N) ∧ (𝑧N𝑤N)) → [⟨((𝑥 ·N 𝑤) +N (𝑦 ·N 𝑧)), (𝑦 ·N 𝑤)⟩] ~Q ∈ ((N × N) / ~Q ))
196, 18eqeltrd 2114 . . 3 (((𝑥N𝑦N) ∧ (𝑧N𝑤N)) → ([⟨𝑥, 𝑦⟩] ~Q +Q [⟨𝑧, 𝑤⟩] ~Q ) ∈ ((N × N) / ~Q ))
201, 3, 5, 192ecoptocl 6157 . 2 ((𝐴Q𝐵Q) → (𝐴 +Q 𝐵) ∈ ((N × N) / ~Q ))
2120, 1syl6eleqr 2131 1 ((𝐴Q𝐵Q) → (𝐴 +Q 𝐵) ∈ Q)