This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 df-ss ⊢ ( 𝐴 ⊆ ( 𝐴 +P 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( 𝐴 +P 𝐵 ) ) )
24 22 23 imbitrrdi ⊢ ( ( 𝐴 ∈ 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 imbitrrdi ⊢ ( ( 𝐴 ∈ 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 𝐵 ) )