Proof of Theorem sltmul2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpl1l 1225 | . . . . 5
⊢ ((((𝐴 ∈ 
No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) ∧ 𝐵 <s 𝐶) → 𝐴 ∈  No
) | 
| 2 |  | simpl3 1194 | . . . . . 6
⊢ ((((𝐴 ∈ 
No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) ∧ 𝐵 <s 𝐶) → 𝐶 ∈  No
) | 
| 3 |  | simpl2 1193 | . . . . . 6
⊢ ((((𝐴 ∈ 
No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) ∧ 𝐵 <s 𝐶) → 𝐵 ∈  No
) | 
| 4 | 2, 3 | subscld 28093 | . . . . 5
⊢ ((((𝐴 ∈ 
No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) ∧ 𝐵 <s 𝐶) → (𝐶 -s 𝐵) ∈  No
) | 
| 5 |  | simpl1r 1226 | . . . . 5
⊢ ((((𝐴 ∈ 
No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) ∧ 𝐵 <s 𝐶) → 0s <s 𝐴) | 
| 6 |  | simp2 1138 | . . . . . . 7
⊢ (((𝐴 ∈ 
No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) → 𝐵 ∈  No
) | 
| 7 |  | simp3 1139 | . . . . . . 7
⊢ (((𝐴 ∈ 
No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) → 𝐶 ∈  No
) | 
| 8 | 6, 7 | posdifsd 28127 | . . . . . 6
⊢ (((𝐴 ∈ 
No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) → (𝐵 <s 𝐶 ↔ 0s <s (𝐶 -s 𝐵))) | 
| 9 | 8 | biimpa 476 | . . . . 5
⊢ ((((𝐴 ∈ 
No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) ∧ 𝐵 <s 𝐶) → 0s <s (𝐶 -s 𝐵)) | 
| 10 | 1, 4, 5, 9 | mulsgt0d 28171 | . . . 4
⊢ ((((𝐴 ∈ 
No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) ∧ 𝐵 <s 𝐶) → 0s <s (𝐴 ·s (𝐶 -s 𝐵))) | 
| 11 | 1, 2, 3 | subsdid 28184 | . . . 4
⊢ ((((𝐴 ∈ 
No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) ∧ 𝐵 <s 𝐶) → (𝐴 ·s (𝐶 -s 𝐵)) = ((𝐴 ·s 𝐶) -s (𝐴 ·s 𝐵))) | 
| 12 | 10, 11 | breqtrd 5169 | . . 3
⊢ ((((𝐴 ∈ 
No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) ∧ 𝐵 <s 𝐶) → 0s <s ((𝐴 ·s 𝐶) -s (𝐴 ·s 𝐵))) | 
| 13 | 1, 3 | mulscld 28161 | . . . 4
⊢ ((((𝐴 ∈ 
No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) ∧ 𝐵 <s 𝐶) → (𝐴 ·s 𝐵) ∈  No
) | 
| 14 | 1, 2 | mulscld 28161 | . . . 4
⊢ ((((𝐴 ∈ 
No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) ∧ 𝐵 <s 𝐶) → (𝐴 ·s 𝐶) ∈  No
) | 
| 15 | 13, 14 | posdifsd 28127 | . . 3
⊢ ((((𝐴 ∈ 
No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) ∧ 𝐵 <s 𝐶) → ((𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶) ↔ 0s <s ((𝐴 ·s 𝐶) -s (𝐴 ·s 𝐵)))) | 
| 16 | 12, 15 | mpbird 257 | . 2
⊢ ((((𝐴 ∈ 
No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) ∧ 𝐵 <s 𝐶) → (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) | 
| 17 |  | simp1l 1198 | . . . . . . . 8
⊢ (((𝐴 ∈ 
No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) → 𝐴 ∈  No
) | 
| 18 | 17, 7 | mulscld 28161 | . . . . . . 7
⊢ (((𝐴 ∈ 
No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) → (𝐴 ·s 𝐶) ∈  No
) | 
| 19 |  | sltirr 27791 | . . . . . . 7
⊢ ((𝐴 ·s 𝐶) ∈ 
No  → ¬ (𝐴
·s 𝐶)
<s (𝐴
·s 𝐶)) | 
| 20 | 18, 19 | syl 17 | . . . . . 6
⊢ (((𝐴 ∈ 
No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) → ¬ (𝐴 ·s 𝐶) <s (𝐴 ·s 𝐶)) | 
| 21 |  | oveq2 7439 | . . . . . . . 8
⊢ (𝐵 = 𝐶 → (𝐴 ·s 𝐵) = (𝐴 ·s 𝐶)) | 
| 22 | 21 | breq1d 5153 | . . . . . . 7
⊢ (𝐵 = 𝐶 → ((𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶) ↔ (𝐴 ·s 𝐶) <s (𝐴 ·s 𝐶))) | 
| 23 | 22 | notbid 318 | . . . . . 6
⊢ (𝐵 = 𝐶 → (¬ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶) ↔ ¬ (𝐴 ·s 𝐶) <s (𝐴 ·s 𝐶))) | 
| 24 | 20, 23 | syl5ibrcom 247 | . . . . 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 406 | . . 3
⊢ ((((𝐴 ∈ 
No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) → ¬ 𝐵 = 𝐶) | 
| 27 | 17, 6 | mulscld 28161 | . . . . . . 7
⊢ (((𝐴 ∈ 
No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) → (𝐴 ·s 𝐵) ∈  No
) | 
| 28 |  | sltasym 27793 | . . . . . . 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 406 | . . . . 5
⊢ ((((𝐴 ∈ 
No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) → ¬ (𝐴 ·s 𝐶) <s (𝐴 ·s 𝐵)) | 
| 31 |  | simpl1l 1225 | . . . . . . . 8
⊢ ((((𝐴 ∈ 
No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) → 𝐴 ∈  No
) | 
| 32 | 31 | adantr 480 | . . . . . . 7
⊢
(((((𝐴 ∈  No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) ∧ 0s <s (𝐵 -s 𝐶)) → 𝐴 ∈  No
) | 
| 33 |  | simpll2 1214 | . . . . . . . 8
⊢
(((((𝐴 ∈  No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) ∧ 0s <s (𝐵 -s 𝐶)) → 𝐵 ∈  No
) | 
| 34 |  | simpll3 1215 | . . . . . . . 8
⊢
(((((𝐴 ∈  No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) ∧ 0s <s (𝐵 -s 𝐶)) → 𝐶 ∈  No
) | 
| 35 | 33, 34 | subscld 28093 | . . . . . . 7
⊢
(((((𝐴 ∈  No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) ∧ 0s <s (𝐵 -s 𝐶)) → (𝐵 -s 𝐶) ∈  No
) | 
| 36 |  | simpl1r 1226 | . . . . . . . 8
⊢ ((((𝐴 ∈ 
No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) → 0s <s 𝐴) | 
| 37 | 36 | adantr 480 | . . . . . . 7
⊢
(((((𝐴 ∈  No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) ∧ 0s <s (𝐵 -s 𝐶)) → 0s <s 𝐴) | 
| 38 |  | simpr 484 | . . . . . . 7
⊢
(((((𝐴 ∈  No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) ∧ 0s <s (𝐵 -s 𝐶)) → 0s <s (𝐵 -s 𝐶)) | 
| 39 | 32, 35, 37, 38 | mulsgt0d 28171 | . . . . . 6
⊢
(((((𝐴 ∈  No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) ∧ 0s <s (𝐵 -s 𝐶)) → 0s <s (𝐴 ·s (𝐵 -s 𝐶))) | 
| 40 | 32, 33, 34 | subsdid 28184 | . . . . . . . 8
⊢
(((((𝐴 ∈  No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) ∧ 0s <s (𝐵 -s 𝐶)) → (𝐴 ·s (𝐵 -s 𝐶)) = ((𝐴 ·s 𝐵) -s (𝐴 ·s 𝐶))) | 
| 41 | 40 | breq2d 5155 | . . . . . . 7
⊢
(((((𝐴 ∈  No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) ∧ 0s <s (𝐵 -s 𝐶)) → ( 0s <s (𝐴 ·s (𝐵 -s 𝐶)) ↔ 0s <s ((𝐴 ·s 𝐵) -s (𝐴 ·s 𝐶)))) | 
| 42 | 18 | ad2antrr 726 | . . . . . . . 8
⊢
(((((𝐴 ∈  No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) ∧ 0s <s (𝐵 -s 𝐶)) → (𝐴 ·s 𝐶) ∈  No
) | 
| 43 | 27 | ad2antrr 726 | . . . . . . . 8
⊢
(((((𝐴 ∈  No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) ∧ 0s <s (𝐵 -s 𝐶)) → (𝐴 ·s 𝐵) ∈  No
) | 
| 44 | 42, 43 | posdifsd 28127 | . . . . . . 7
⊢
(((((𝐴 ∈  No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) ∧ 0s <s (𝐵 -s 𝐶)) → ((𝐴 ·s 𝐶) <s (𝐴 ·s 𝐵) ↔ 0s <s ((𝐴 ·s 𝐵) -s (𝐴 ·s 𝐶)))) | 
| 45 | 41, 44 | bitr4d 282 | . . . . . 6
⊢
(((((𝐴 ∈  No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) ∧ 0s <s (𝐵 -s 𝐶)) → ( 0s <s (𝐴 ·s (𝐵 -s 𝐶)) ↔ (𝐴 ·s 𝐶) <s (𝐴 ·s 𝐵))) | 
| 46 | 39, 45 | mpbid 232 | . . . . 5
⊢
(((((𝐴 ∈  No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) ∧ 0s <s (𝐵 -s 𝐶)) → (𝐴 ·s 𝐶) <s (𝐴 ·s 𝐵)) | 
| 47 | 30, 46 | mtand 816 | . . . 4
⊢ ((((𝐴 ∈ 
No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) → ¬ 0s <s (𝐵 -s 𝐶)) | 
| 48 |  | simpl3 1194 | . . . . 5
⊢ ((((𝐴 ∈ 
No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) → 𝐶 ∈  No
) | 
| 49 |  | simpl2 1193 | . . . . 5
⊢ ((((𝐴 ∈ 
No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) → 𝐵 ∈  No
) | 
| 50 | 48, 49 | posdifsd 28127 | . . . 4
⊢ ((((𝐴 ∈ 
No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) → (𝐶 <s 𝐵 ↔ 0s <s (𝐵 -s 𝐶))) | 
| 51 | 47, 50 | mtbird 325 | . . 3
⊢ ((((𝐴 ∈ 
No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) → ¬ 𝐶 <s 𝐵) | 
| 52 |  | sltlin 27794 | . . . 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 1475 | . 2
⊢ ((((𝐴 ∈ 
No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) ∧ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶)) → 𝐵 <s 𝐶) | 
| 55 | 16, 54 | impbida 801 | 1
⊢ (((𝐴 ∈ 
No  ∧ 0s <s 𝐴) ∧ 𝐵 ∈  No 
∧ 𝐶 ∈  No ) → (𝐵 <s 𝐶 ↔ (𝐴 ·s 𝐵) <s (𝐴 ·s 𝐶))) |