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

 Description: Closure of addition on positive reals. First statement of Proposition 9-3.5 of [Gleason] p. 123. Combination of Lemma 11.13 and Lemma 11.16 in [BauerTaylor], p. 53. (Contributed by NM, 13-Mar-1996.)
Assertion
Ref Expression
addclpr ((𝐴P𝐵P) → (𝐴 +P 𝐵) ∈ P)

Proof of Theorem addclpr
Dummy variables 𝑥 𝑦 𝑧 𝑤 𝑣 𝑔 𝑞 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-iplp 7288 . . . 4 +P = (𝑤P, 𝑣P ↦ ⟨{𝑥Q ∣ ∃𝑦Q𝑧Q (𝑦 ∈ (1st𝑤) ∧ 𝑧 ∈ (1st𝑣) ∧ 𝑥 = (𝑦 +Q 𝑧))}, {𝑥Q ∣ ∃𝑦Q𝑧Q (𝑦 ∈ (2nd𝑤) ∧ 𝑧 ∈ (2nd𝑣) ∧ 𝑥 = (𝑦 +Q 𝑧))}⟩)
21genpelxp 7331 . . 3 ((𝐴P𝐵P) → (𝐴 +P 𝐵) ∈ (𝒫 Q × 𝒫 Q))
3 addclnq 7195 . . . 4 ((𝑦Q𝑧Q) → (𝑦 +Q 𝑧) ∈ Q)
41, 3genpml 7337 . . 3 ((𝐴P𝐵P) → ∃𝑞Q 𝑞 ∈ (1st ‘(𝐴 +P 𝐵)))
51, 3genpmu 7338 . . 3 ((𝐴P𝐵P) → ∃𝑟Q 𝑟 ∈ (2nd ‘(𝐴 +P 𝐵)))
62, 4, 5jca32 308 . 2 ((𝐴P𝐵P) → ((𝐴 +P 𝐵) ∈ (𝒫 Q × 𝒫 Q) ∧ (∃𝑞Q 𝑞 ∈ (1st ‘(𝐴 +P 𝐵)) ∧ ∃𝑟Q 𝑟 ∈ (2nd ‘(𝐴 +P 𝐵)))))
7 ltanqg 7220 . . . . 5 ((𝑥Q𝑦Q𝑧Q) → (𝑥 <Q 𝑦 ↔ (𝑧 +Q 𝑥) <Q (𝑧 +Q 𝑦)))
8 addcomnqg 7201 . . . . 5 ((𝑥Q𝑦Q) → (𝑥 +Q 𝑦) = (𝑦 +Q 𝑥))
9 addnqprl 7349 . . . . 5 ((((𝐴P𝑔 ∈ (1st𝐴)) ∧ (𝐵P ∈ (1st𝐵))) ∧ 𝑥Q) → (𝑥 <Q (𝑔 +Q ) → 𝑥 ∈ (1st ‘(𝐴 +P 𝐵))))
101, 3, 7, 8, 9genprndl 7341 . . . 4 ((𝐴P𝐵P) → ∀𝑞Q (𝑞 ∈ (1st ‘(𝐴 +P 𝐵)) ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟 ∈ (1st ‘(𝐴 +P 𝐵)))))
11 addnqpru 7350 . . . . 5 ((((𝐴P𝑔 ∈ (2nd𝐴)) ∧ (𝐵P ∈ (2nd𝐵))) ∧ 𝑥Q) → ((𝑔 +Q ) <Q 𝑥𝑥 ∈ (2nd ‘(𝐴 +P 𝐵))))
121, 3, 7, 8, 11genprndu 7342 . . . 4 ((𝐴P𝐵P) → ∀𝑟Q (𝑟 ∈ (2nd ‘(𝐴 +P 𝐵)) ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd ‘(𝐴 +P 𝐵)))))
1310, 12jca 304 . . 3 ((𝐴P𝐵P) → (∀𝑞Q (𝑞 ∈ (1st ‘(𝐴 +P 𝐵)) ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟 ∈ (1st ‘(𝐴 +P 𝐵)))) ∧ ∀𝑟Q (𝑟 ∈ (2nd ‘(𝐴 +P 𝐵)) ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd ‘(𝐴 +P 𝐵))))))
141, 3, 7, 8genpdisj 7343 . . 3 ((𝐴P𝐵P) → ∀𝑞Q ¬ (𝑞 ∈ (1st ‘(𝐴 +P 𝐵)) ∧ 𝑞 ∈ (2nd ‘(𝐴 +P 𝐵))))
15 addlocpr 7356 . . 3 ((𝐴P𝐵P) → ∀𝑞Q𝑟Q (𝑞 <Q 𝑟 → (𝑞 ∈ (1st ‘(𝐴 +P 𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴 +P 𝐵)))))
1613, 14, 153jca 1161 . 2 ((𝐴P𝐵P) → ((∀𝑞Q (𝑞 ∈ (1st ‘(𝐴 +P 𝐵)) ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟 ∈ (1st ‘(𝐴 +P 𝐵)))) ∧ ∀𝑟Q (𝑟 ∈ (2nd ‘(𝐴 +P 𝐵)) ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd ‘(𝐴 +P 𝐵))))) ∧ ∀𝑞Q ¬ (𝑞 ∈ (1st ‘(𝐴 +P 𝐵)) ∧ 𝑞 ∈ (2nd ‘(𝐴 +P 𝐵))) ∧ ∀𝑞Q𝑟Q (𝑞 <Q 𝑟 → (𝑞 ∈ (1st ‘(𝐴 +P 𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴 +P 𝐵))))))
17 elnp1st2nd 7296 . 2 ((𝐴 +P 𝐵) ∈ P ↔ (((𝐴 +P 𝐵) ∈ (𝒫 Q × 𝒫 Q) ∧ (∃𝑞Q 𝑞 ∈ (1st ‘(𝐴 +P 𝐵)) ∧ ∃𝑟Q 𝑟 ∈ (2nd ‘(𝐴 +P 𝐵)))) ∧ ((∀𝑞Q (𝑞 ∈ (1st ‘(𝐴 +P 𝐵)) ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟 ∈ (1st ‘(𝐴 +P 𝐵)))) ∧ ∀𝑟Q (𝑟 ∈ (2nd ‘(𝐴 +P 𝐵)) ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd ‘(𝐴 +P 𝐵))))) ∧ ∀𝑞Q ¬ (𝑞 ∈ (1st ‘(𝐴 +P 𝐵)) ∧ 𝑞 ∈ (2nd ‘(𝐴 +P 𝐵))) ∧ ∀𝑞Q𝑟Q (𝑞 <Q 𝑟 → (𝑞 ∈ (1st ‘(𝐴 +P 𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴 +P 𝐵)))))))
186, 16, 17sylanbrc 413 1 ((𝐴P𝐵P) → (𝐴 +P 𝐵) ∈ P)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 697   ∧ w3a 962   ∈ wcel 1480  ∀wral 2416  ∃wrex 2417  𝒫 cpw 3510   class class class wbr 3929   × cxp 4537  ‘cfv 5123  (class class class)co 5774  1st c1st 6036  2nd c2nd 6037  Qcnq 7100   +Q cplq 7102
 Copyright terms: Public domain W3C validator