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

Metamath Proof Explorer

Theorem ltaprlem

Description: Lemma for Proposition 9-3.5(v) of Gleason p. 123. (Contributed by NM, 8-Apr-1996) (New usage is discouraged.)

Ref Expression
Assertion ltaprlem ⊢ C ∈ 𝑷 → A < 𝑷 B → C + 𝑷 A < 𝑷 C + 𝑷 B

Proof

Step Hyp Ref Expression
1 ltrelpr ⊢ < 𝑷 ⊆ 𝑷 × 𝑷
2 1 brel ⊢ A < 𝑷 B → A ∈ 𝑷 ∧ B ∈ 𝑷
3 2 simpld ⊢ A < 𝑷 B → A ∈ 𝑷
4 ltexpri ⊢ A < 𝑷 B → ∃ x ∈ 𝑷 A + 𝑷 x = B
5 addclpr ⊢ C ∈ 𝑷 ∧ A ∈ 𝑷 → C + 𝑷 A ∈ 𝑷
6 ltaddpr ⊢ C + 𝑷 A ∈ 𝑷 ∧ x ∈ 𝑷 → C + 𝑷 A < 𝑷 C + 𝑷 A + 𝑷 x
7 addasspr ⊢ C + 𝑷 A + 𝑷 x = C + 𝑷 A + 𝑷 x
8 oveq2 ⊢ A + 𝑷 x = B → C + 𝑷 A + 𝑷 x = C + 𝑷 B
9 7 8 eqtrid ⊢ A + 𝑷 x = B → C + 𝑷 A + 𝑷 x = C + 𝑷 B
10 9 breq2d ⊢ A + 𝑷 x = B → C + 𝑷 A < 𝑷 C + 𝑷 A + 𝑷 x ↔ C + 𝑷 A < 𝑷 C + 𝑷 B
11 6 10 imbitrid ⊢ A + 𝑷 x = B → C + 𝑷 A ∈ 𝑷 ∧ x ∈ 𝑷 → C + 𝑷 A < 𝑷 C + 𝑷 B
12 11 expd ⊢ A + 𝑷 x = B → C + 𝑷 A ∈ 𝑷 → x ∈ 𝑷 → C + 𝑷 A < 𝑷 C + 𝑷 B
13 5 12 syl5 ⊢ A + 𝑷 x = B → C ∈ 𝑷 ∧ A ∈ 𝑷 → x ∈ 𝑷 → C + 𝑷 A < 𝑷 C + 𝑷 B
14 13 com3r ⊢ x ∈ 𝑷 → A + 𝑷 x = B → C ∈ 𝑷 ∧ A ∈ 𝑷 → C + 𝑷 A < 𝑷 C + 𝑷 B
15 14 rexlimiv ⊢ ∃ x ∈ 𝑷 A + 𝑷 x = B → C ∈ 𝑷 ∧ A ∈ 𝑷 → C + 𝑷 A < 𝑷 C + 𝑷 B
16 4 15 syl ⊢ A < 𝑷 B → C ∈ 𝑷 ∧ A ∈ 𝑷 → C + 𝑷 A < 𝑷 C + 𝑷 B
17 3 16 sylan2i ⊢ A < 𝑷 B → C ∈ 𝑷 ∧ A < 𝑷 B → C + 𝑷 A < 𝑷 C + 𝑷 B
18 17 expd ⊢ A < 𝑷 B → C ∈ 𝑷 → A < 𝑷 B → C + 𝑷 A < 𝑷 C + 𝑷 B
19 18 pm2.43b ⊢ C ∈ 𝑷 → A < 𝑷 B → C + 𝑷 A < 𝑷 C + 𝑷 B