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 ((A P B P) → (A +P B) P)

Dummy variables x y z w v g 𝑞 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-iplp 6451 . . . 4 +P = (w P, v P ↦ ⟨{x Qy Q z Q (y (1stw) z (1stv) x = (y +Q z))}, {x Qy Q z Q (y (2ndw) z (2ndv) x = (y +Q z))}⟩)
21genpelxp 6494 . . 3 ((A P B P) → (A +P B) (𝒫 Q × 𝒫 Q))
3 addclnq 6359 . . . 4 ((y Q z Q) → (y +Q z) Q)
41, 3genpml 6500 . . 3 ((A P B P) → 𝑞 Q 𝑞 (1st ‘(A +P B)))
51, 3genpmu 6501 . . 3 ((A P B P) → 𝑟 Q 𝑟 (2nd ‘(A +P B)))
62, 4, 5jca32 293 . 2 ((A P B P) → ((A +P B) (𝒫 Q × 𝒫 Q) (𝑞 Q 𝑞 (1st ‘(A +P B)) 𝑟 Q 𝑟 (2nd ‘(A +P B)))))
7 ltanqg 6384 . . . . 5 ((x Q y Q z Q) → (x <Q y ↔ (z +Q x) <Q (z +Q y)))
8 addcomnqg 6365 . . . . 5 ((x Q y Q) → (x +Q y) = (y +Q x))
9 addnqprl 6512 . . . . 5 ((((A P g (1stA)) (B P (1stB))) x Q) → (x <Q (g +Q ) → x (1st ‘(A +P B))))
101, 3, 7, 8, 9genprndl 6504 . . . 4 ((A P B P) → 𝑞 Q (𝑞 (1st ‘(A +P B)) ↔ 𝑟 Q (𝑞 <Q 𝑟 𝑟 (1st ‘(A +P B)))))
11 addnqpru 6513 . . . . 5 ((((A P g (2ndA)) (B P (2ndB))) x Q) → ((g +Q ) <Q xx (2nd ‘(A +P B))))
121, 3, 7, 8, 11genprndu 6505 . . . 4 ((A P B P) → 𝑟 Q (𝑟 (2nd ‘(A +P B)) ↔ 𝑞 Q (𝑞 <Q 𝑟 𝑞 (2nd ‘(A +P B)))))
1310, 12jca 290 . . 3 ((A P B P) → (𝑞 Q (𝑞 (1st ‘(A +P B)) ↔ 𝑟 Q (𝑞 <Q 𝑟 𝑟 (1st ‘(A +P B)))) 𝑟 Q (𝑟 (2nd ‘(A +P B)) ↔ 𝑞 Q (𝑞 <Q 𝑟 𝑞 (2nd ‘(A +P B))))))
141, 3, 7, 8genpdisj 6506 . . 3 ((A P B P) → 𝑞 Q ¬ (𝑞 (1st ‘(A +P B)) 𝑞 (2nd ‘(A +P B))))
15 addlocpr 6519 . . 3 ((A P B P) → 𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 (1st ‘(A +P B)) 𝑟 (2nd ‘(A +P B)))))
1613, 14, 153jca 1083 . 2 ((A P B P) → ((𝑞 Q (𝑞 (1st ‘(A +P B)) ↔ 𝑟 Q (𝑞 <Q 𝑟 𝑟 (1st ‘(A +P B)))) 𝑟 Q (𝑟 (2nd ‘(A +P B)) ↔ 𝑞 Q (𝑞 <Q 𝑟 𝑞 (2nd ‘(A +P B))))) 𝑞 Q ¬ (𝑞 (1st ‘(A +P B)) 𝑞 (2nd ‘(A +P B))) 𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 (1st ‘(A +P B)) 𝑟 (2nd ‘(A +P B))))))
17 elnp1st2nd 6459 . 2 ((A +P B) P ↔ (((A +P B) (𝒫 Q × 𝒫 Q) (𝑞 Q 𝑞 (1st ‘(A +P B)) 𝑟 Q 𝑟 (2nd ‘(A +P B)))) ((𝑞 Q (𝑞 (1st ‘(A +P B)) ↔ 𝑟 Q (𝑞 <Q 𝑟 𝑟 (1st ‘(A +P B)))) 𝑟 Q (𝑟 (2nd ‘(A +P B)) ↔ 𝑞 Q (𝑞 <Q 𝑟 𝑞 (2nd ‘(A +P B))))) 𝑞 Q ¬ (𝑞 (1st ‘(A +P B)) 𝑞 (2nd ‘(A +P B))) 𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 (1st ‘(A +P B)) 𝑟 (2nd ‘(A +P B)))))))
186, 16, 17sylanbrc 394 1 ((A P B P) → (A +P B) P)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ↔ wb 98   ∨ wo 628   ∧ w3a 884   ∈ wcel 1390  ∀wral 2300  ∃wrex 2301  𝒫 cpw 3351   class class class wbr 3755   × cxp 4286  ‘cfv 4845  (class class class)co 5455  1st c1st 5707  2nd c2nd 5708  Qcnq 6264   +Q cplq 6266
 Copyright terms: Public domain W3C validator