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

 Description: Addition to both sides of 'less than'. (Contributed by NM, 12-Nov-1999.) (Revised by Mario Carneiro, 27-May-2016.)
Assertion
Ref Expression
ltadd2 ((A B 𝐶 ℝ) → (A < B ↔ (𝐶 + A) < (𝐶 + B)))

Proof of Theorem ltadd2
Dummy variable x is distinct from all other variables.
StepHypRef Expression
1 axltadd 6689 . 2 ((A B 𝐶 ℝ) → (A < B → (𝐶 + A) < (𝐶 + B)))
2 ax-rnegex 6596 . . . 4 (𝐶 ℝ → x ℝ (𝐶 + x) = 0)
323ad2ant3 909 . . 3 ((A B 𝐶 ℝ) → x ℝ (𝐶 + x) = 0)
4 simpl3 891 . . . . . . 7 (((A B 𝐶 ℝ) (x (𝐶 + x) = 0)) → 𝐶 ℝ)
5 simpl1 889 . . . . . . 7 (((A B 𝐶 ℝ) (x (𝐶 + x) = 0)) → A ℝ)
64, 5readdcld 6655 . . . . . 6 (((A B 𝐶 ℝ) (x (𝐶 + x) = 0)) → (𝐶 + A) ℝ)
7 simpl2 890 . . . . . . 7 (((A B 𝐶 ℝ) (x (𝐶 + x) = 0)) → B ℝ)
84, 7readdcld 6655 . . . . . 6 (((A B 𝐶 ℝ) (x (𝐶 + x) = 0)) → (𝐶 + B) ℝ)
9 simprl 468 . . . . . 6 (((A B 𝐶 ℝ) (x (𝐶 + x) = 0)) → x ℝ)
10 axltadd 6689 . . . . . 6 (((𝐶 + A) (𝐶 + B) x ℝ) → ((𝐶 + A) < (𝐶 + B) → (x + (𝐶 + A)) < (x + (𝐶 + B))))
116, 8, 9, 10syl3anc 1116 . . . . 5 (((A B 𝐶 ℝ) (x (𝐶 + x) = 0)) → ((𝐶 + A) < (𝐶 + B) → (x + (𝐶 + A)) < (x + (𝐶 + B))))
129recnd 6654 . . . . . . 7 (((A B 𝐶 ℝ) (x (𝐶 + x) = 0)) → x ℂ)
134recnd 6654 . . . . . . 7 (((A B 𝐶 ℝ) (x (𝐶 + x) = 0)) → 𝐶 ℂ)
145recnd 6654 . . . . . . 7 (((A B 𝐶 ℝ) (x (𝐶 + x) = 0)) → A ℂ)
1512, 13, 14addassd 6650 . . . . . 6 (((A B 𝐶 ℝ) (x (𝐶 + x) = 0)) → ((x + 𝐶) + A) = (x + (𝐶 + A)))
167recnd 6654 . . . . . . 7 (((A B 𝐶 ℝ) (x (𝐶 + x) = 0)) → B ℂ)
1712, 13, 16addassd 6650 . . . . . 6 (((A B 𝐶 ℝ) (x (𝐶 + x) = 0)) → ((x + 𝐶) + B) = (x + (𝐶 + B)))
1815, 17breq12d 3740 . . . . 5 (((A B 𝐶 ℝ) (x (𝐶 + x) = 0)) → (((x + 𝐶) + A) < ((x + 𝐶) + B) ↔ (x + (𝐶 + A)) < (x + (𝐶 + B))))
1911, 18sylibrd 158 . . . 4 (((A B 𝐶 ℝ) (x (𝐶 + x) = 0)) → ((𝐶 + A) < (𝐶 + B) → ((x + 𝐶) + A) < ((x + 𝐶) + B)))
20 simprr 469 . . . . . . . 8 (((A B 𝐶 ℝ) (x (𝐶 + x) = 0)) → (𝐶 + x) = 0)
21 addcom 6750 . . . . . . . . . 10 ((𝐶 x ℂ) → (𝐶 + x) = (x + 𝐶))
2221eqeq1d 2021 . . . . . . . . 9 ((𝐶 x ℂ) → ((𝐶 + x) = 0 ↔ (x + 𝐶) = 0))
2313, 12, 22syl2anc 391 . . . . . . . 8 (((A B 𝐶 ℝ) (x (𝐶 + x) = 0)) → ((𝐶 + x) = 0 ↔ (x + 𝐶) = 0))
2420, 23mpbid 135 . . . . . . 7 (((A B 𝐶 ℝ) (x (𝐶 + x) = 0)) → (x + 𝐶) = 0)
2524oveq1d 5439 . . . . . 6 (((A B 𝐶 ℝ) (x (𝐶 + x) = 0)) → ((x + 𝐶) + A) = (0 + A))
2614addid2d 6763 . . . . . 6 (((A B 𝐶 ℝ) (x (𝐶 + x) = 0)) → (0 + A) = A)
2725, 26eqtrd 2045 . . . . 5 (((A B 𝐶 ℝ) (x (𝐶 + x) = 0)) → ((x + 𝐶) + A) = A)
2824oveq1d 5439 . . . . . 6 (((A B 𝐶 ℝ) (x (𝐶 + x) = 0)) → ((x + 𝐶) + B) = (0 + B))
2916addid2d 6763 . . . . . 6 (((A B 𝐶 ℝ) (x (𝐶 + x) = 0)) → (0 + B) = B)
3028, 29eqtrd 2045 . . . . 5 (((A B 𝐶 ℝ) (x (𝐶 + x) = 0)) → ((x + 𝐶) + B) = B)
3127, 30breq12d 3740 . . . 4 (((A B 𝐶 ℝ) (x (𝐶 + x) = 0)) → (((x + 𝐶) + A) < ((x + 𝐶) + B) ↔ A < B))
3219, 31sylibd 138 . . 3 (((A B 𝐶 ℝ) (x (𝐶 + x) = 0)) → ((𝐶 + A) < (𝐶 + B) → A < B))
333, 32rexlimddv 2406 . 2 ((A B 𝐶 ℝ) → ((𝐶 + A) < (𝐶 + B) → A < B))
341, 33impbid 120 1 ((A B 𝐶 ℝ) → (A < B ↔ (𝐶 + A) < (𝐶 + B)))