Proof of Theorem sltmul2
Step | Hyp | Ref
| Expression |
1 | | simpl1l 1224 |
. . . . 5
⊢ ((((𝐴 ∈
No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ 𝐵 <s 𝐶) → 𝐴 ∈ No
) |
2 | | simpl3 1193 |
. . . . . 6
⊢ ((((𝐴 ∈
No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ 𝐵 <s 𝐶) → 𝐶 ∈ No
) |
3 | | simpl2 1192 |
. . . . . 6
⊢ ((((𝐴 ∈
No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ 𝐵 <s 𝐶) → 𝐵 ∈ No
) |
4 | 2, 3 | subscld 27464 |
. . . . 5
⊢ ((((𝐴 ∈
No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ 𝐵 <s 𝐶) → (𝐶 -s 𝐵) ∈ No
) |
5 | | simpl1r 1225 |
. . . . 5
⊢ ((((𝐴 ∈
No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ 𝐵 <s 𝐶) → 0s <s 𝐴) |
6 | | simp2 1137 |
. . . . . . 7
⊢ (((𝐴 ∈
No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) → 𝐵 ∈ No
) |
7 | | simp3 1138 |
. . . . . . 7
⊢ (((𝐴 ∈
No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) → 𝐶 ∈ No
) |
8 | 6, 7 | posdifsd 27490 |
. . . . . 6
⊢ (((𝐴 ∈
No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) → (𝐵 <s 𝐶 ↔ 0s <s (𝐶 -s 𝐵))) |
9 | 8 | biimpa 477 |
. . . . 5
⊢ ((((𝐴 ∈
No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ 𝐵 <s 𝐶) → 0s <s (𝐶 -s 𝐵)) |
10 | 1, 4, 5, 9 | mulsgt0d 27530 |
. . . 4
⊢ ((((𝐴 ∈
No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ 𝐵 <s 𝐶) → 0s <s (𝐴 ·s (𝐶 -s 𝐵))) |
11 | 1, 2, 3 | subsdid 27542 |
. . . 4
⊢ ((((𝐴 ∈
No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ 𝐵 <s 𝐶) → (𝐴 ·s (𝐶 -s 𝐵)) = ((𝐴 ·s 𝐶) -s (𝐴 ·s 𝐵))) |
12 | 10, 11 | breqtrd 5168 |
. . 3
⊢ ((((𝐴 ∈
No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ 𝐵 <s 𝐶) → 0s <s ((𝐴 ·s 𝐶) -s (𝐴 ·s 𝐵))) |
13 | 1, 3 | mulscld 27520 |
. . . 4
⊢ ((((𝐴 ∈
No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ 𝐵 <s 𝐶) → (𝐴 ·s 𝐵) ∈ No
) |
14 | 1, 2 | mulscld 27520 |
. . . 4
⊢ ((((𝐴 ∈
No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ 𝐵 <s 𝐶) → (𝐴 ·s 𝐶) ∈ No
) |
15 | 13, 14 | posdifsd 27490 |
. . 3
⊢ ((((𝐴 ∈
No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ 𝐵 <s 𝐶) → ((𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶) ↔ 0s <s ((𝐴 ·s 𝐶) -s (𝐴 ·s 𝐵)))) |
16 | 12, 15 | mpbird 256 |
. 2
⊢ ((((𝐴 ∈
No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ 𝐵 <s 𝐶) → (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) |
17 | | simp1l 1197 |
. . . . . . . 8
⊢ (((𝐴 ∈
No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) → 𝐴 ∈ No
) |
18 | 17, 7 | mulscld 27520 |
. . . . . . 7
⊢ (((𝐴 ∈
No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) → (𝐴 ·s 𝐶) ∈ No
) |
19 | | sltirr 27178 |
. . . . . . 7
⊢ ((𝐴 ·s 𝐶) ∈
No → ¬ (𝐴
·s 𝐶)
<s (𝐴
·s 𝐶)) |
20 | 18, 19 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈
No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) → ¬ (𝐴 ·s 𝐶) <s (𝐴 ·s 𝐶)) |
21 | | oveq2 7402 |
. . . . . . . 8
⊢ (𝐵 = 𝐶 → (𝐴 ·s 𝐵) = (𝐴 ·s 𝐶)) |
22 | 21 | breq1d 5152 |
. . . . . . 7
⊢ (𝐵 = 𝐶 → ((𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶) ↔ (𝐴 ·s 𝐶) <s (𝐴 ·s 𝐶))) |
23 | 22 | notbid 317 |
. . . . . 6
⊢ (𝐵 = 𝐶 → (¬ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶) ↔ ¬ (𝐴 ·s 𝐶) <s (𝐴 ·s 𝐶))) |
24 | 20, 23 | syl5ibrcom 246 |
. . . . 5
⊢ (((𝐴 ∈
No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) → (𝐵 = 𝐶 → ¬ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶))) |
25 | 24 | con2d 134 |
. . . 4
⊢ (((𝐴 ∈
No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) → ((𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶) → ¬ 𝐵 = 𝐶)) |
26 | 25 | imp 407 |
. . 3
⊢ ((((𝐴 ∈
No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) → ¬ 𝐵 = 𝐶) |
27 | 17, 6 | mulscld 27520 |
. . . . . . 7
⊢ (((𝐴 ∈
No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) → (𝐴 ·s 𝐵) ∈ No
) |
28 | | sltasym 27180 |
. . . . . . 7
⊢ (((𝐴 ·s 𝐵) ∈
No ∧ (𝐴
·s 𝐶)
∈ No ) → ((𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶) → ¬ (𝐴 ·s 𝐶) <s (𝐴 ·s 𝐵))) |
29 | 27, 18, 28 | syl2anc 584 |
. . . . . 6
⊢ (((𝐴 ∈
No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) → ((𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶) → ¬ (𝐴 ·s 𝐶) <s (𝐴 ·s 𝐵))) |
30 | 29 | imp 407 |
. . . . 5
⊢ ((((𝐴 ∈
No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) → ¬ (𝐴 ·s 𝐶) <s (𝐴 ·s 𝐵)) |
31 | | simpl1l 1224 |
. . . . . . . 8
⊢ ((((𝐴 ∈
No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) → 𝐴 ∈ No
) |
32 | 31 | adantr 481 |
. . . . . . 7
⊢
(((((𝐴 ∈ No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) ∧ 0s <s (𝐵 -s 𝐶)) → 𝐴 ∈ No
) |
33 | | simpll2 1213 |
. . . . . . . 8
⊢
(((((𝐴 ∈ No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) ∧ 0s <s (𝐵 -s 𝐶)) → 𝐵 ∈ No
) |
34 | | simpll3 1214 |
. . . . . . . 8
⊢
(((((𝐴 ∈ No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) ∧ 0s <s (𝐵 -s 𝐶)) → 𝐶 ∈ No
) |
35 | 33, 34 | subscld 27464 |
. . . . . . 7
⊢
(((((𝐴 ∈ No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) ∧ 0s <s (𝐵 -s 𝐶)) → (𝐵 -s 𝐶) ∈ No
) |
36 | | simpl1r 1225 |
. . . . . . . 8
⊢ ((((𝐴 ∈
No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) → 0s <s 𝐴) |
37 | 36 | adantr 481 |
. . . . . . 7
⊢
(((((𝐴 ∈ No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) ∧ 0s <s (𝐵 -s 𝐶)) → 0s <s 𝐴) |
38 | | simpr 485 |
. . . . . . 7
⊢
(((((𝐴 ∈ No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) ∧ 0s <s (𝐵 -s 𝐶)) → 0s <s (𝐵 -s 𝐶)) |
39 | 32, 35, 37, 38 | mulsgt0d 27530 |
. . . . . 6
⊢
(((((𝐴 ∈ No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) ∧ 0s <s (𝐵 -s 𝐶)) → 0s <s (𝐴 ·s (𝐵 -s 𝐶))) |
40 | 32, 33, 34 | subsdid 27542 |
. . . . . . . 8
⊢
(((((𝐴 ∈ No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) ∧ 0s <s (𝐵 -s 𝐶)) → (𝐴 ·s (𝐵 -s 𝐶)) = ((𝐴 ·s 𝐵) -s (𝐴 ·s 𝐶))) |
41 | 40 | breq2d 5154 |
. . . . . . 7
⊢
(((((𝐴 ∈ No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) ∧ 0s <s (𝐵 -s 𝐶)) → ( 0s <s (𝐴 ·s (𝐵 -s 𝐶)) ↔ 0s <s ((𝐴 ·s 𝐵) -s (𝐴 ·s 𝐶)))) |
42 | 18 | ad2antrr 724 |
. . . . . . . 8
⊢
(((((𝐴 ∈ No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) ∧ 0s <s (𝐵 -s 𝐶)) → (𝐴 ·s 𝐶) ∈ No
) |
43 | 27 | ad2antrr 724 |
. . . . . . . 8
⊢
(((((𝐴 ∈ No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) ∧ 0s <s (𝐵 -s 𝐶)) → (𝐴 ·s 𝐵) ∈ No
) |
44 | 42, 43 | posdifsd 27490 |
. . . . . . 7
⊢
(((((𝐴 ∈ No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) ∧ 0s <s (𝐵 -s 𝐶)) → ((𝐴 ·s 𝐶) <s (𝐴 ·s 𝐵) ↔ 0s <s ((𝐴 ·s 𝐵) -s (𝐴 ·s 𝐶)))) |
45 | 41, 44 | bitr4d 281 |
. . . . . 6
⊢
(((((𝐴 ∈ No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) ∧ 0s <s (𝐵 -s 𝐶)) → ( 0s <s (𝐴 ·s (𝐵 -s 𝐶)) ↔ (𝐴 ·s 𝐶) <s (𝐴 ·s 𝐵))) |
46 | 39, 45 | mpbid 231 |
. . . . 5
⊢
(((((𝐴 ∈ No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) ∧ 0s <s (𝐵 -s 𝐶)) → (𝐴 ·s 𝐶) <s (𝐴 ·s 𝐵)) |
47 | 30, 46 | mtand 814 |
. . . 4
⊢ ((((𝐴 ∈
No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) → ¬ 0s <s (𝐵 -s 𝐶)) |
48 | | simpl3 1193 |
. . . . 5
⊢ ((((𝐴 ∈
No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) → 𝐶 ∈ No
) |
49 | | simpl2 1192 |
. . . . 5
⊢ ((((𝐴 ∈
No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) → 𝐵 ∈ No
) |
50 | 48, 49 | posdifsd 27490 |
. . . 4
⊢ ((((𝐴 ∈
No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) → (𝐶 <s 𝐵 ↔ 0s <s (𝐵 -s 𝐶))) |
51 | 47, 50 | mtbird 324 |
. . 3
⊢ ((((𝐴 ∈
No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) → ¬ 𝐶 <s 𝐵) |
52 | | sltlin 27181 |
. . . 4
⊢ ((𝐵 ∈
No ∧ 𝐶 ∈
No ) → (𝐵 <s 𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶 <s 𝐵)) |
53 | 49, 48, 52 | syl2anc 584 |
. . 3
⊢ ((((𝐴 ∈
No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) → (𝐵 <s 𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶 <s 𝐵)) |
54 | 26, 51, 53 | ecase23d 1473 |
. 2
⊢ ((((𝐴 ∈
No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) → 𝐵 <s 𝐶) |
55 | 16, 54 | impbida 799 |
1
⊢ (((𝐴 ∈
No ∧ 0s <s 𝐴) ∧ 𝐵 ∈ No
∧ 𝐶 ∈ No ) → (𝐵 <s 𝐶 ↔ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶))) |