Proof of Theorem ltmpig
Step | Hyp | Ref
| Expression |
1 | | pinn 6293 |
. . . . 5
⊢ (A ∈
N → A ∈ 𝜔) |
2 | | pinn 6293 |
. . . . 5
⊢ (B ∈
N → B ∈ 𝜔) |
3 | | elni2 6298 |
. . . . . 6
⊢ (𝐶 ∈ N ↔ (𝐶 ∈
𝜔 ∧ ∅ ∈ 𝐶)) |
4 | | iba 284 |
. . . . . . . . 9
⊢ (∅
∈ 𝐶 → (A ∈ B ↔ (A
∈ B ∧ ∅ ∈ 𝐶))) |
5 | | nnmord 6026 |
. . . . . . . . 9
⊢
((A ∈ 𝜔 ∧
B ∈
𝜔 ∧ 𝐶 ∈
𝜔) → ((A ∈ B ∧ ∅ ∈ 𝐶) ↔ (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
B))) |
6 | 4, 5 | sylan9bbr 436 |
. . . . . . . 8
⊢
(((A ∈ 𝜔 ∧
B ∈
𝜔 ∧ 𝐶 ∈
𝜔) ∧ ∅ ∈ 𝐶) → (A ∈ B ↔ (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
B))) |
7 | 6 | 3exp1 1119 |
. . . . . . 7
⊢ (A ∈ 𝜔
→ (B ∈ 𝜔 → (𝐶 ∈
𝜔 → (∅ ∈ 𝐶 → (A ∈ B ↔ (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
B)))))) |
8 | 7 | imp4b 332 |
. . . . . 6
⊢
((A ∈ 𝜔 ∧
B ∈
𝜔) → ((𝐶 ∈ 𝜔 ∧
∅ ∈ 𝐶) → (A ∈ B ↔ (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
B)))) |
9 | 3, 8 | syl5bi 141 |
. . . . 5
⊢
((A ∈ 𝜔 ∧
B ∈
𝜔) → (𝐶 ∈ N → (A ∈ B ↔ (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
B)))) |
10 | 1, 2, 9 | syl2an 273 |
. . . 4
⊢
((A ∈ N ∧ B ∈ N) → (𝐶 ∈
N → (A ∈ B ↔
(𝐶
·𝑜 A) ∈ (𝐶 ·𝑜 B)))) |
11 | 10 | imp 115 |
. . 3
⊢
(((A ∈ N ∧ B ∈ N) ∧ 𝐶 ∈
N) → (A ∈ B ↔
(𝐶
·𝑜 A) ∈ (𝐶 ·𝑜 B))) |
12 | | ltpiord 6303 |
. . . 4
⊢
((A ∈ N ∧ B ∈ N) → (A <N B ↔ A ∈ B)) |
13 | 12 | adantr 261 |
. . 3
⊢
(((A ∈ N ∧ B ∈ N) ∧ 𝐶 ∈
N) → (A
<N B ↔
A ∈
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))) |
17 | 14, 15, 16 | syl2an 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)) |
19 | 18 | adantr 261 |
. . . . . . 7
⊢ (((𝐶 ∈ N ∧ A ∈ N) ∧ (𝐶 ∈
N ∧ B ∈
N)) → (𝐶
·N A) =
(𝐶
·𝑜 A)) |
20 | | mulpiord 6301 |
. . . . . . . 8
⊢ ((𝐶 ∈ N ∧ B ∈ N) → (𝐶 ·N B) = (𝐶 ·𝑜 B)) |
21 | 20 | adantl 262 |
. . . . . . 7
⊢ (((𝐶 ∈ N ∧ A ∈ N) ∧ (𝐶 ∈
N ∧ B ∈
N)) → (𝐶
·N B) =
(𝐶
·𝑜 B)) |
22 | 19, 21 | eleq12d 2105 |
. . . . . 6
⊢ (((𝐶 ∈ N ∧ A ∈ N) ∧ (𝐶 ∈
N ∧ B ∈
N)) → ((𝐶 ·N A) ∈ (𝐶
·N B)
↔ (𝐶
·𝑜 A) ∈ (𝐶 ·𝑜 B))) |
23 | 17, 22 | bitrd 177 |
. . . . 5
⊢ (((𝐶 ∈ N ∧ A ∈ N) ∧ (𝐶 ∈
N ∧ B ∈
N)) → ((𝐶 ·N A) <N (𝐶 ·N B) ↔ (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
B))) |
24 | 23 | anandis 526 |
. . . 4
⊢ ((𝐶 ∈ N ∧ (A ∈ N ∧ B ∈ N)) → ((𝐶 ·N A) <N (𝐶 ·N B) ↔ (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
B))) |
25 | 24 | ancoms 255 |
. . 3
⊢
(((A ∈ N ∧ B ∈ N) ∧ 𝐶 ∈
N) → ((𝐶
·N A)
<N (𝐶 ·N B) ↔ (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
B))) |
26 | 11, 13, 25 | 3bitr4d 209 |
. 2
⊢
(((A ∈ N ∧ B ∈ N) ∧ 𝐶 ∈
N) → (A
<N B ↔
(𝐶
·N A)
<N (𝐶 ·N B))) |
27 | 26 | 3impa 1098 |
1
⊢
((A ∈ N ∧ B ∈ N ∧ 𝐶 ∈
N) → (A
<N B ↔
(𝐶
·N A)
<N (𝐶 ·N B))) |