Metamath Proof Explorer


Theorem ltaddpr

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) (New usage is discouraged.)

Ref Expression
Assertion ltaddpr ( ( 𝐴P𝐵P ) → 𝐴 <P ( 𝐴 +P 𝐵 ) )

Proof

Step Hyp Ref Expression
1 prn0 ( 𝐵P𝐵 ≠ ∅ )
2 n0 ( 𝐵 ≠ ∅ ↔ ∃ 𝑦 𝑦𝐵 )
3 1 2 sylib ( 𝐵P → ∃ 𝑦 𝑦𝐵 )
4 3 adantl ( ( 𝐴P𝐵P ) → ∃ 𝑦 𝑦𝐵 )
5 addclpr ( ( 𝐴P𝐵P ) → ( 𝐴 +P 𝐵 ) ∈ P )
6 df-plp +P = ( 𝑤P , 𝑣P ↦ { 𝑥 ∣ ∃ 𝑦𝑤𝑧𝑣 𝑥 = ( 𝑦 +Q 𝑧 ) } )
7 addclnq ( ( 𝑦Q𝑧Q ) → ( 𝑦 +Q 𝑧 ) ∈ Q )
8 6 7 genpprecl ( ( 𝐴P𝐵P ) → ( ( 𝑥𝐴𝑦𝐵 ) → ( 𝑥 +Q 𝑦 ) ∈ ( 𝐴 +P 𝐵 ) ) )
9 8 imp ( ( ( 𝐴P𝐵P ) ∧ ( 𝑥𝐴𝑦𝐵 ) ) → ( 𝑥 +Q 𝑦 ) ∈ ( 𝐴 +P 𝐵 ) )
10 elprnq ( ( ( 𝐴 +P 𝐵 ) ∈ P ∧ ( 𝑥 +Q 𝑦 ) ∈ ( 𝐴 +P 𝐵 ) ) → ( 𝑥 +Q 𝑦 ) ∈ Q )
11 addnqf +Q : ( Q × Q ) ⟶ Q
12 11 fdmi dom +Q = ( Q × Q )
13 0nnq ¬ ∅ ∈ Q
14 12 13 ndmovrcl ( ( 𝑥 +Q 𝑦 ) ∈ Q → ( 𝑥Q𝑦Q ) )
15 ltaddnq ( ( 𝑥Q𝑦Q ) → 𝑥 <Q ( 𝑥 +Q 𝑦 ) )
16 10 14 15 3syl ( ( ( 𝐴 +P 𝐵 ) ∈ P ∧ ( 𝑥 +Q 𝑦 ) ∈ ( 𝐴 +P 𝐵 ) ) → 𝑥 <Q ( 𝑥 +Q 𝑦 ) )
17 prcdnq ( ( ( 𝐴 +P 𝐵 ) ∈ P ∧ ( 𝑥 +Q 𝑦 ) ∈ ( 𝐴 +P 𝐵 ) ) → ( 𝑥 <Q ( 𝑥 +Q 𝑦 ) → 𝑥 ∈ ( 𝐴 +P 𝐵 ) ) )
18 16 17 mpd ( ( ( 𝐴 +P 𝐵 ) ∈ P ∧ ( 𝑥 +Q 𝑦 ) ∈ ( 𝐴 +P 𝐵 ) ) → 𝑥 ∈ ( 𝐴 +P 𝐵 ) )
19 5 9 18 syl2an2r ( ( ( 𝐴P𝐵P ) ∧ ( 𝑥𝐴𝑦𝐵 ) ) → 𝑥 ∈ ( 𝐴 +P 𝐵 ) )
20 19 exp32 ( ( 𝐴P𝐵P ) → ( 𝑥𝐴 → ( 𝑦𝐵𝑥 ∈ ( 𝐴 +P 𝐵 ) ) ) )
21 20 com23 ( ( 𝐴P𝐵P ) → ( 𝑦𝐵 → ( 𝑥𝐴𝑥 ∈ ( 𝐴 +P 𝐵 ) ) ) )
22 21 alrimdv ( ( 𝐴P𝐵P ) → ( 𝑦𝐵 → ∀ 𝑥 ( 𝑥𝐴𝑥 ∈ ( 𝐴 +P 𝐵 ) ) ) )
23 dfss2 ( 𝐴 ⊆ ( 𝐴 +P 𝐵 ) ↔ ∀ 𝑥 ( 𝑥𝐴𝑥 ∈ ( 𝐴 +P 𝐵 ) ) )
24 22 23 syl6ibr ( ( 𝐴P𝐵P ) → ( 𝑦𝐵𝐴 ⊆ ( 𝐴 +P 𝐵 ) ) )
25 vex 𝑦 ∈ V
26 25 prlem934 ( 𝐴P → ∃ 𝑥𝐴 ¬ ( 𝑥 +Q 𝑦 ) ∈ 𝐴 )
27 26 adantr ( ( 𝐴P𝐵P ) → ∃ 𝑥𝐴 ¬ ( 𝑥 +Q 𝑦 ) ∈ 𝐴 )
28 eleq2 ( 𝐴 = ( 𝐴 +P 𝐵 ) → ( ( 𝑥 +Q 𝑦 ) ∈ 𝐴 ↔ ( 𝑥 +Q 𝑦 ) ∈ ( 𝐴 +P 𝐵 ) ) )
29 28 biimprcd ( ( 𝑥 +Q 𝑦 ) ∈ ( 𝐴 +P 𝐵 ) → ( 𝐴 = ( 𝐴 +P 𝐵 ) → ( 𝑥 +Q 𝑦 ) ∈ 𝐴 ) )
30 29 con3d ( ( 𝑥 +Q 𝑦 ) ∈ ( 𝐴 +P 𝐵 ) → ( ¬ ( 𝑥 +Q 𝑦 ) ∈ 𝐴 → ¬ 𝐴 = ( 𝐴 +P 𝐵 ) ) )
31 8 30 syl6 ( ( 𝐴P𝐵P ) → ( ( 𝑥𝐴𝑦𝐵 ) → ( ¬ ( 𝑥 +Q 𝑦 ) ∈ 𝐴 → ¬ 𝐴 = ( 𝐴 +P 𝐵 ) ) ) )
32 31 expd ( ( 𝐴P𝐵P ) → ( 𝑥𝐴 → ( 𝑦𝐵 → ( ¬ ( 𝑥 +Q 𝑦 ) ∈ 𝐴 → ¬ 𝐴 = ( 𝐴 +P 𝐵 ) ) ) ) )
33 32 com34 ( ( 𝐴P𝐵P ) → ( 𝑥𝐴 → ( ¬ ( 𝑥 +Q 𝑦 ) ∈ 𝐴 → ( 𝑦𝐵 → ¬ 𝐴 = ( 𝐴 +P 𝐵 ) ) ) ) )
34 33 rexlimdv ( ( 𝐴P𝐵P ) → ( ∃ 𝑥𝐴 ¬ ( 𝑥 +Q 𝑦 ) ∈ 𝐴 → ( 𝑦𝐵 → ¬ 𝐴 = ( 𝐴 +P 𝐵 ) ) ) )
35 27 34 mpd ( ( 𝐴P𝐵P ) → ( 𝑦𝐵 → ¬ 𝐴 = ( 𝐴 +P 𝐵 ) ) )
36 24 35 jcad ( ( 𝐴P𝐵P ) → ( 𝑦𝐵 → ( 𝐴 ⊆ ( 𝐴 +P 𝐵 ) ∧ ¬ 𝐴 = ( 𝐴 +P 𝐵 ) ) ) )
37 dfpss2 ( 𝐴 ⊊ ( 𝐴 +P 𝐵 ) ↔ ( 𝐴 ⊆ ( 𝐴 +P 𝐵 ) ∧ ¬ 𝐴 = ( 𝐴 +P 𝐵 ) ) )
38 36 37 syl6ibr ( ( 𝐴P𝐵P ) → ( 𝑦𝐵𝐴 ⊊ ( 𝐴 +P 𝐵 ) ) )
39 38 exlimdv ( ( 𝐴P𝐵P ) → ( ∃ 𝑦 𝑦𝐵𝐴 ⊊ ( 𝐴 +P 𝐵 ) ) )
40 4 39 mpd ( ( 𝐴P𝐵P ) → 𝐴 ⊊ ( 𝐴 +P 𝐵 ) )
41 ltprord ( ( 𝐴P ∧ ( 𝐴 +P 𝐵 ) ∈ P ) → ( 𝐴 <P ( 𝐴 +P 𝐵 ) ↔ 𝐴 ⊊ ( 𝐴 +P 𝐵 ) ) )
42 5 41 syldan ( ( 𝐴P𝐵P ) → ( 𝐴 <P ( 𝐴 +P 𝐵 ) ↔ 𝐴 ⊊ ( 𝐴 +P 𝐵 ) ) )
43 40 42 mpbird ( ( 𝐴P𝐵P ) → 𝐴 <P ( 𝐴 +P 𝐵 ) )