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

Theorem ltmpig 6323
 Description: Ordering property of multiplication for positive integers. (Contributed by Jim Kingdon, 31-Aug-2019.)
Assertion
Ref Expression
ltmpig ((A N B N 𝐶 N) → (A <N B ↔ (𝐶 ·N A) <N (𝐶 ·N B)))

Proof of Theorem ltmpig
StepHypRef Expression
1 pinn 6293 . . . . 5 (A NA 𝜔)
2 pinn 6293 . . . . 5 (B NB 𝜔)
3 elni2 6298 . . . . . 6 (𝐶 N ↔ (𝐶 𝜔 𝐶))
4 iba 284 . . . . . . . . 9 (∅ 𝐶 → (A B ↔ (A B 𝐶)))
5 nnmord 6026 . . . . . . . . 9 ((A 𝜔 B 𝜔 𝐶 𝜔) → ((A B 𝐶) ↔ (𝐶 ·𝑜 A) (𝐶 ·𝑜 B)))
64, 5sylan9bbr 436 . . . . . . . 8 (((A 𝜔 B 𝜔 𝐶 𝜔) 𝐶) → (A B ↔ (𝐶 ·𝑜 A) (𝐶 ·𝑜 B)))
763exp1 1119 . . . . . . 7 (A 𝜔 → (B 𝜔 → (𝐶 𝜔 → (∅ 𝐶 → (A B ↔ (𝐶 ·𝑜 A) (𝐶 ·𝑜 B))))))
87imp4b 332 . . . . . 6 ((A 𝜔 B 𝜔) → ((𝐶 𝜔 𝐶) → (A B ↔ (𝐶 ·𝑜 A) (𝐶 ·𝑜 B))))
93, 8syl5bi 141 . . . . 5 ((A 𝜔 B 𝜔) → (𝐶 N → (A B ↔ (𝐶 ·𝑜 A) (𝐶 ·𝑜 B))))
101, 2, 9syl2an 273 . . . 4 ((A N B N) → (𝐶 N → (A B ↔ (𝐶 ·𝑜 A) (𝐶 ·𝑜 B))))
1110imp 115 . . 3 (((A N B N) 𝐶 N) → (A B ↔ (𝐶 ·𝑜 A) (𝐶 ·𝑜 B)))
12 ltpiord 6303 . . . 4 ((A N B N) → (A <N BA B))
1312adantr 261 . . 3 (((A N B N) 𝐶 N) → (A <N BA B))
14 mulclpi 6312 . . . . . . 7 ((𝐶 N A N) → (𝐶 ·N A) N)
15 mulclpi 6312 . . . . . . 7 ((𝐶 N B N) → (𝐶 ·N B) N)
16 ltpiord 6303 . . . . . . 7 (((𝐶 ·N A) N (𝐶 ·N B) N) → ((𝐶 ·N A) <N (𝐶 ·N B) ↔ (𝐶 ·N A) (𝐶 ·N B)))
1714, 15, 16syl2an 273 . . . . . 6 (((𝐶 N A N) (𝐶 N B N)) → ((𝐶 ·N A) <N (𝐶 ·N B) ↔ (𝐶 ·N A) (𝐶 ·N B)))
18 mulpiord 6301 . . . . . . . 8 ((𝐶 N A N) → (𝐶 ·N A) = (𝐶 ·𝑜 A))
1918adantr 261 . . . . . . 7 (((𝐶 N A N) (𝐶 N B N)) → (𝐶 ·N A) = (𝐶 ·𝑜 A))
20 mulpiord 6301 . . . . . . . 8 ((𝐶 N B N) → (𝐶 ·N B) = (𝐶 ·𝑜 B))
2120adantl 262 . . . . . . 7 (((𝐶 N A N) (𝐶 N B N)) → (𝐶 ·N B) = (𝐶 ·𝑜 B))
2219, 21eleq12d 2105 . . . . . 6 (((𝐶 N A N) (𝐶 N B N)) → ((𝐶 ·N A) (𝐶 ·N B) ↔ (𝐶 ·𝑜 A) (𝐶 ·𝑜 B)))
2317, 22bitrd 177 . . . . 5 (((𝐶 N A N) (𝐶 N B N)) → ((𝐶 ·N A) <N (𝐶 ·N B) ↔ (𝐶 ·𝑜 A) (𝐶 ·𝑜 B)))
2423anandis 526 . . . 4 ((𝐶 N (A N B N)) → ((𝐶 ·N A) <N (𝐶 ·N B) ↔ (𝐶 ·𝑜 A) (𝐶 ·𝑜 B)))
2524ancoms 255 . . 3 (((A N B N) 𝐶 N) → ((𝐶 ·N A) <N (𝐶 ·N B) ↔ (𝐶 ·𝑜 A) (𝐶 ·𝑜 B)))
2611, 13, 253bitr4d 209 . 2 (((A N B N) 𝐶 N) → (A <N B ↔ (𝐶 ·N A) <N (𝐶 ·N B)))
27263impa 1098 1 ((A N B N 𝐶 N) → (A <N B ↔ (𝐶 ·N A) <N (𝐶 ·N B)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∧ w3a 884   = wceq 1242   ∈ wcel 1390  ∅c0 3218   class class class wbr 3755  𝜔com 4256  (class class class)co 5455   ·𝑜 comu 5938  Ncnpi 6256   ·N cmi 6258
 Copyright terms: Public domain W3C validator