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

 Description: The sum of two positive reals is greater than one of them. Proposition 9-3.5(iii) of [Gleason] p. 123. (Contributed by NM, 26-Mar-1996.) (Revised by Mario Carneiro, 12-Jun-2013.)
Assertion
Ref Expression
ltaddpr ((A P B P) → A<P (A +P B))

Dummy variables f g x y 𝑝 𝑞 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prop 6458 . . . 4 (B P → ⟨(1stB), (2ndB)⟩ P)
2 prml 6460 . . . 4 (⟨(1stB), (2ndB)⟩ P𝑝 Q 𝑝 (1stB))
31, 2syl 14 . . 3 (B P𝑝 Q 𝑝 (1stB))
43adantl 262 . 2 ((A P B P) → 𝑝 Q 𝑝 (1stB))
5 prop 6458 . . . . 5 (A P → ⟨(1stA), (2ndA)⟩ P)
6 prarloc 6486 . . . . 5 ((⟨(1stA), (2ndA)⟩ P 𝑝 Q) → 𝑟 (1stA)𝑞 (2ndA)𝑞 <Q (𝑟 +Q 𝑝))
75, 6sylan 267 . . . 4 ((A P 𝑝 Q) → 𝑟 (1stA)𝑞 (2ndA)𝑞 <Q (𝑟 +Q 𝑝))
87ad2ant2r 478 . . 3 (((A P B P) (𝑝 Q 𝑝 (1stB))) → 𝑟 (1stA)𝑞 (2ndA)𝑞 <Q (𝑟 +Q 𝑝))
9 elprnqu 6465 . . . . . . . . . . 11 ((⟨(1stA), (2ndA)⟩ P 𝑞 (2ndA)) → 𝑞 Q)
105, 9sylan 267 . . . . . . . . . 10 ((A P 𝑞 (2ndA)) → 𝑞 Q)
1110adantlr 446 . . . . . . . . 9 (((A P B P) 𝑞 (2ndA)) → 𝑞 Q)
1211ad2ant2rl 480 . . . . . . . 8 ((((A P B P) (𝑝 Q 𝑝 (1stB))) (𝑟 (1stA) 𝑞 (2ndA))) → 𝑞 Q)
1312adantr 261 . . . . . . 7 (((((A P B P) (𝑝 Q 𝑝 (1stB))) (𝑟 (1stA) 𝑞 (2ndA))) 𝑞 <Q (𝑟 +Q 𝑝)) → 𝑞 Q)
14 simplrr 488 . . . . . . 7 (((((A P B P) (𝑝 Q 𝑝 (1stB))) (𝑟 (1stA) 𝑞 (2ndA))) 𝑞 <Q (𝑟 +Q 𝑝)) → 𝑞 (2ndA))
15 simprl 483 . . . . . . . . . . . . 13 (((𝑝 Q 𝑝 (1stB)) (𝑟 (1stA) 𝑞 (2ndA))) → 𝑟 (1stA))
16 simplr 482 . . . . . . . . . . . . 13 (((𝑝 Q 𝑝 (1stB)) (𝑟 (1stA) 𝑞 (2ndA))) → 𝑝 (1stB))
1715, 16jca 290 . . . . . . . . . . . 12 (((𝑝 Q 𝑝 (1stB)) (𝑟 (1stA) 𝑞 (2ndA))) → (𝑟 (1stA) 𝑝 (1stB)))
18 df-iplp 6451 . . . . . . . . . . . . 13 +P = (x P, y P ↦ ⟨{f Qg Q Q (g (1stx) (1sty) f = (g +Q ))}, {f Qg Q Q (g (2ndx) (2ndy) f = (g +Q ))}⟩)
19 addclnq 6359 . . . . . . . . . . . . 13 ((g Q Q) → (g +Q ) Q)
2018, 19genpprecll 6497 . . . . . . . . . . . 12 ((A P B P) → ((𝑟 (1stA) 𝑝 (1stB)) → (𝑟 +Q 𝑝) (1st ‘(A +P B))))
2117, 20syl5 28 . . . . . . . . . . 11 ((A P B P) → (((𝑝 Q 𝑝 (1stB)) (𝑟 (1stA) 𝑞 (2ndA))) → (𝑟 +Q 𝑝) (1st ‘(A +P B))))
2221imdistani 419 . . . . . . . . . 10 (((A P B P) ((𝑝 Q 𝑝 (1stB)) (𝑟 (1stA) 𝑞 (2ndA)))) → ((A P B P) (𝑟 +Q 𝑝) (1st ‘(A +P B))))
23 addclpr 6520 . . . . . . . . . . 11 ((A P B P) → (A +P B) P)
24 prop 6458 . . . . . . . . . . . 12 ((A +P B) P → ⟨(1st ‘(A +P B)), (2nd ‘(A +P B))⟩ P)
25 prcdnql 6467 . . . . . . . . . . . 12 ((⟨(1st ‘(A +P B)), (2nd ‘(A +P B))⟩ P (𝑟 +Q 𝑝) (1st ‘(A +P B))) → (𝑞 <Q (𝑟 +Q 𝑝) → 𝑞 (1st ‘(A +P B))))
2624, 25sylan 267 . . . . . . . . . . 11 (((A +P B) P (𝑟 +Q 𝑝) (1st ‘(A +P B))) → (𝑞 <Q (𝑟 +Q 𝑝) → 𝑞 (1st ‘(A +P B))))
2723, 26sylan 267 . . . . . . . . . 10 (((A P B P) (𝑟 +Q 𝑝) (1st ‘(A +P B))) → (𝑞 <Q (𝑟 +Q 𝑝) → 𝑞 (1st ‘(A +P B))))
2822, 27syl 14 . . . . . . . . 9 (((A P B P) ((𝑝 Q 𝑝 (1stB)) (𝑟 (1stA) 𝑞 (2ndA)))) → (𝑞 <Q (𝑟 +Q 𝑝) → 𝑞 (1st ‘(A +P B))))
2928anassrs 380 . . . . . . . 8 ((((A P B P) (𝑝 Q 𝑝 (1stB))) (𝑟 (1stA) 𝑞 (2ndA))) → (𝑞 <Q (𝑟 +Q 𝑝) → 𝑞 (1st ‘(A +P B))))
3029imp 115 . . . . . . 7 (((((A P B P) (𝑝 Q 𝑝 (1stB))) (𝑟 (1stA) 𝑞 (2ndA))) 𝑞 <Q (𝑟 +Q 𝑝)) → 𝑞 (1st ‘(A +P B)))
31 rspe 2364 . . . . . . 7 ((𝑞 Q (𝑞 (2ndA) 𝑞 (1st ‘(A +P B)))) → 𝑞 Q (𝑞 (2ndA) 𝑞 (1st ‘(A +P B))))
3213, 14, 30, 31syl12anc 1132 . . . . . 6 (((((A P B P) (𝑝 Q 𝑝 (1stB))) (𝑟 (1stA) 𝑞 (2ndA))) 𝑞 <Q (𝑟 +Q 𝑝)) → 𝑞 Q (𝑞 (2ndA) 𝑞 (1st ‘(A +P B))))
33 ltdfpr 6489 . . . . . . . 8 ((A P (A +P B) P) → (A<P (A +P B) ↔ 𝑞 Q (𝑞 (2ndA) 𝑞 (1st ‘(A +P B)))))
3423, 33syldan 266 . . . . . . 7 ((A P B P) → (A<P (A +P B) ↔ 𝑞 Q (𝑞 (2ndA) 𝑞 (1st ‘(A +P B)))))
3534ad3antrrr 461 . . . . . 6 (((((A P B P) (𝑝 Q 𝑝 (1stB))) (𝑟 (1stA) 𝑞 (2ndA))) 𝑞 <Q (𝑟 +Q 𝑝)) → (A<P (A +P B) ↔ 𝑞 Q (𝑞 (2ndA) 𝑞 (1st ‘(A +P B)))))
3632, 35mpbird 156 . . . . 5 (((((A P B P) (𝑝 Q 𝑝 (1stB))) (𝑟 (1stA) 𝑞 (2ndA))) 𝑞 <Q (𝑟 +Q 𝑝)) → A<P (A +P B))
3736ex 108 . . . 4 ((((A P B P) (𝑝 Q 𝑝 (1stB))) (𝑟 (1stA) 𝑞 (2ndA))) → (𝑞 <Q (𝑟 +Q 𝑝) → A<P (A +P B)))
3837rexlimdvva 2434 . . 3 (((A P B P) (𝑝 Q 𝑝 (1stB))) → (𝑟 (1stA)𝑞 (2ndA)𝑞 <Q (𝑟 +Q 𝑝) → A<P (A +P B)))
398, 38mpd 13 . 2 (((A P B P) (𝑝 Q 𝑝 (1stB))) → A<P (A +P B))
404, 39rexlimddv 2431 1 ((A P B P) → A<P (A +P B))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∈ wcel 1390  ∃wrex 2301  ⟨cop 3370   class class class wbr 3755  ‘cfv 4845  (class class class)co 5455  1st c1st 5707  2nd c2nd 5708  Qcnq 6264   +Q cplq 6266
 Copyright terms: Public domain W3C validator