Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ltaprlem Structured version   Visualization version   GIF version

Theorem ltaprlem 9745
 Description: Lemma for Proposition 9-3.5(v) of [Gleason] p. 123. (Contributed by NM, 8-Apr-1996.) (New usage is discouraged.)
Assertion
Ref Expression
ltaprlem (𝐶P → (𝐴<P 𝐵 → (𝐶 +P 𝐴)<P (𝐶 +P 𝐵)))

Proof of Theorem ltaprlem
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 ltrelpr 9699 . . . . . 6 <P ⊆ (P × P)
21brel 5090 . . . . 5 (𝐴<P 𝐵 → (𝐴P𝐵P))
32simpld 474 . . . 4 (𝐴<P 𝐵𝐴P)
4 ltexpri 9744 . . . . 5 (𝐴<P 𝐵 → ∃𝑥P (𝐴 +P 𝑥) = 𝐵)
5 addclpr 9719 . . . . . . . 8 ((𝐶P𝐴P) → (𝐶 +P 𝐴) ∈ P)
6 ltaddpr 9735 . . . . . . . . . 10 (((𝐶 +P 𝐴) ∈ P𝑥P) → (𝐶 +P 𝐴)<P ((𝐶 +P 𝐴) +P 𝑥))
7 addasspr 9723 . . . . . . . . . . . 12 ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P (𝐴 +P 𝑥))
8 oveq2 6557 . . . . . . . . . . . 12 ((𝐴 +P 𝑥) = 𝐵 → (𝐶 +P (𝐴 +P 𝑥)) = (𝐶 +P 𝐵))
97, 8syl5eq 2656 . . . . . . . . . . 11 ((𝐴 +P 𝑥) = 𝐵 → ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P 𝐵))
109breq2d 4595 . . . . . . . . . 10 ((𝐴 +P 𝑥) = 𝐵 → ((𝐶 +P 𝐴)<P ((𝐶 +P 𝐴) +P 𝑥) ↔ (𝐶 +P 𝐴)<P (𝐶 +P 𝐵)))
116, 10syl5ib 233 . . . . . . . . 9 ((𝐴 +P 𝑥) = 𝐵 → (((𝐶 +P 𝐴) ∈ P𝑥P) → (𝐶 +P 𝐴)<P (𝐶 +P 𝐵)))
1211expd 451 . . . . . . . 8 ((𝐴 +P 𝑥) = 𝐵 → ((𝐶 +P 𝐴) ∈ P → (𝑥P → (𝐶 +P 𝐴)<P (𝐶 +P 𝐵))))
135, 12syl5 33 . . . . . . 7 ((𝐴 +P 𝑥) = 𝐵 → ((𝐶P𝐴P) → (𝑥P → (𝐶 +P 𝐴)<P (𝐶 +P 𝐵))))
1413com3r 85 . . . . . 6 (𝑥P → ((𝐴 +P 𝑥) = 𝐵 → ((𝐶P𝐴P) → (𝐶 +P 𝐴)<P (𝐶 +P 𝐵))))
1514rexlimiv 3009 . . . . 5 (∃𝑥P (𝐴 +P 𝑥) = 𝐵 → ((𝐶P𝐴P) → (𝐶 +P 𝐴)<P (𝐶 +P 𝐵)))
164, 15syl 17 . . . 4 (𝐴<P 𝐵 → ((𝐶P𝐴P) → (𝐶 +P 𝐴)<P (𝐶 +P 𝐵)))
173, 16sylan2i 685 . . 3 (𝐴<P 𝐵 → ((𝐶P𝐴<P 𝐵) → (𝐶 +P 𝐴)<P (𝐶 +P 𝐵)))
1817expd 451 . 2 (𝐴<P 𝐵 → (𝐶P → (𝐴<P 𝐵 → (𝐶 +P 𝐴)<P (𝐶 +P 𝐵))))
1918pm2.43b 53 1 (𝐶P → (𝐴<P 𝐵 → (𝐶 +P 𝐴)<P (𝐶 +P 𝐵)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∃wrex 2897   class class class wbr 4583  (class class class)co 6549  Pcnp 9560   +P cpp 9562
 Copyright terms: Public domain W3C validator