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

Theorem ltaprlem 6591
 Description: Lemma for Proposition 9-3.5(v) of [Gleason] p. 123. (Contributed by NM, 8-Apr-1996.)
Assertion
Ref Expression
ltaprlem (𝐶 P → (A<P B → (𝐶 +P A)<P (𝐶 +P B)))

Proof of Theorem ltaprlem
Dummy variable x is distinct from all other variables.
StepHypRef Expression
1 ltexpri 6587 . . . 4 (A<P Bx P (A +P x) = B)
21adantr 261 . . 3 ((A<P B 𝐶 P) → x P (A +P x) = B)
3 simplr 482 . . . . . 6 (((A<P B 𝐶 P) (x P (A +P x) = B)) → 𝐶 P)
4 ltrelpr 6488 . . . . . . . . . 10 <P ⊆ (P × P)
54brel 4335 . . . . . . . . 9 (A<P B → (A P B P))
65simpld 105 . . . . . . . 8 (A<P BA P)
76adantr 261 . . . . . . 7 ((A<P B 𝐶 P) → A P)
87adantr 261 . . . . . 6 (((A<P B 𝐶 P) (x P (A +P x) = B)) → A P)
9 addclpr 6520 . . . . . 6 ((𝐶 P A P) → (𝐶 +P A) P)
103, 8, 9syl2anc 391 . . . . 5 (((A<P B 𝐶 P) (x P (A +P x) = B)) → (𝐶 +P A) P)
11 simprl 483 . . . . 5 (((A<P B 𝐶 P) (x P (A +P x) = B)) → x P)
12 ltaddpr 6571 . . . . 5 (((𝐶 +P A) P x P) → (𝐶 +P A)<P ((𝐶 +P A) +P x))
1310, 11, 12syl2anc 391 . . . 4 (((A<P B 𝐶 P) (x P (A +P x) = B)) → (𝐶 +P A)<P ((𝐶 +P A) +P x))
14 addassprg 6555 . . . . . 6 ((𝐶 P A P x P) → ((𝐶 +P A) +P x) = (𝐶 +P (A +P x)))
153, 8, 11, 14syl3anc 1134 . . . . 5 (((A<P B 𝐶 P) (x P (A +P x) = B)) → ((𝐶 +P A) +P x) = (𝐶 +P (A +P x)))
16 oveq2 5463 . . . . . 6 ((A +P x) = B → (𝐶 +P (A +P x)) = (𝐶 +P B))
1716ad2antll 460 . . . . 5 (((A<P B 𝐶 P) (x P (A +P x) = B)) → (𝐶 +P (A +P x)) = (𝐶 +P B))
1815, 17eqtrd 2069 . . . 4 (((A<P B 𝐶 P) (x P (A +P x) = B)) → ((𝐶 +P A) +P x) = (𝐶 +P B))
1913, 18breqtrd 3779 . . 3 (((A<P B 𝐶 P) (x P (A +P x) = B)) → (𝐶 +P A)<P (𝐶 +P B))
202, 19rexlimddv 2431 . 2 ((A<P B 𝐶 P) → (𝐶 +P A)<P (𝐶 +P B))
2120expcom 109 1 (𝐶 P → (A<P B → (𝐶 +P A)<P (𝐶 +P B)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   = wceq 1242   ∈ wcel 1390  ∃wrex 2301   class class class wbr 3755  (class class class)co 5455  Pcnp 6275   +P cpp 6277
 Copyright terms: Public domain W3C validator