Proof of Theorem mulscan2d
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mulscan2d.3 | . . . . 5
⊢ (𝜑 → 𝐶 ∈  No
) | 
| 2 |  | 0sno 27871 | . . . . 5
⊢ 
0s ∈  No | 
| 3 |  | sltneg 28077 | . . . . 5
⊢ ((𝐶 ∈ 
No  ∧ 0s ∈  No ) →
(𝐶 <s 0s
↔ ( -us ‘ 0s ) <s ( -us
‘𝐶))) | 
| 4 | 1, 2, 3 | sylancl 586 | . . . 4
⊢ (𝜑 → (𝐶 <s 0s ↔ ( -us
‘ 0s ) <s ( -us ‘𝐶))) | 
| 5 |  | negs0s 28058 | . . . . 5
⊢ (
-us ‘ 0s ) = 0s | 
| 6 | 5 | breq1i 5150 | . . . 4
⊢ ((
-us ‘ 0s ) <s ( -us ‘𝐶) ↔ 0s <s (
-us ‘𝐶)) | 
| 7 | 4, 6 | bitrdi 287 | . . 3
⊢ (𝜑 → (𝐶 <s 0s ↔ 0s
<s ( -us ‘𝐶))) | 
| 8 |  | mulscan2d.1 | . . . . . . . 8
⊢ (𝜑 → 𝐴 ∈  No
) | 
| 9 | 8, 1 | mulnegs2d 28187 | . . . . . . 7
⊢ (𝜑 → (𝐴 ·s ( -us
‘𝐶)) = (
-us ‘(𝐴
·s 𝐶))) | 
| 10 |  | mulscan2d.2 | . . . . . . . 8
⊢ (𝜑 → 𝐵 ∈  No
) | 
| 11 | 10, 1 | mulnegs2d 28187 | . . . . . . 7
⊢ (𝜑 → (𝐵 ·s ( -us
‘𝐶)) = (
-us ‘(𝐵
·s 𝐶))) | 
| 12 | 9, 11 | eqeq12d 2753 | . . . . . 6
⊢ (𝜑 → ((𝐴 ·s ( -us
‘𝐶)) = (𝐵 ·s (
-us ‘𝐶))
↔ ( -us ‘(𝐴 ·s 𝐶)) = ( -us ‘(𝐵 ·s 𝐶)))) | 
| 13 | 8, 1 | mulscld 28161 | . . . . . . 7
⊢ (𝜑 → (𝐴 ·s 𝐶) ∈  No
) | 
| 14 | 10, 1 | mulscld 28161 | . . . . . . 7
⊢ (𝜑 → (𝐵 ·s 𝐶) ∈  No
) | 
| 15 |  | negs11 28081 | . . . . . . 7
⊢ (((𝐴 ·s 𝐶) ∈ 
No  ∧ (𝐵
·s 𝐶)
∈  No ) → (( -us
‘(𝐴
·s 𝐶)) =
( -us ‘(𝐵
·s 𝐶))
↔ (𝐴
·s 𝐶) =
(𝐵 ·s
𝐶))) | 
| 16 | 13, 14, 15 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → (( -us
‘(𝐴
·s 𝐶)) =
( -us ‘(𝐵
·s 𝐶))
↔ (𝐴
·s 𝐶) =
(𝐵 ·s
𝐶))) | 
| 17 | 12, 16 | bitrd 279 | . . . . 5
⊢ (𝜑 → ((𝐴 ·s ( -us
‘𝐶)) = (𝐵 ·s (
-us ‘𝐶))
↔ (𝐴
·s 𝐶) =
(𝐵 ·s
𝐶))) | 
| 18 | 17 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 0s <s (
-us ‘𝐶))
→ ((𝐴
·s ( -us ‘𝐶)) = (𝐵 ·s ( -us
‘𝐶)) ↔ (𝐴 ·s 𝐶) = (𝐵 ·s 𝐶))) | 
| 19 | 8 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 0s <s (
-us ‘𝐶))
→ 𝐴 ∈  No ) | 
| 20 | 10 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 0s <s (
-us ‘𝐶))
→ 𝐵 ∈  No ) | 
| 21 | 1 | negscld 28069 | . . . . . 6
⊢ (𝜑 → ( -us
‘𝐶) ∈  No ) | 
| 22 | 21 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 0s <s (
-us ‘𝐶))
→ ( -us ‘𝐶) ∈  No
) | 
| 23 |  | simpr 484 | . . . . 5
⊢ ((𝜑 ∧ 0s <s (
-us ‘𝐶))
→ 0s <s ( -us ‘𝐶)) | 
| 24 | 19, 20, 22, 23 | mulscan2dlem 28204 | . . . 4
⊢ ((𝜑 ∧ 0s <s (
-us ‘𝐶))
→ ((𝐴
·s ( -us ‘𝐶)) = (𝐵 ·s ( -us
‘𝐶)) ↔ 𝐴 = 𝐵)) | 
| 25 | 18, 24 | bitr3d 281 | . . 3
⊢ ((𝜑 ∧ 0s <s (
-us ‘𝐶))
→ ((𝐴
·s 𝐶) =
(𝐵 ·s
𝐶) ↔ 𝐴 = 𝐵)) | 
| 26 | 7, 25 | sylbida 592 | . 2
⊢ ((𝜑 ∧ 𝐶 <s 0s ) → ((𝐴 ·s 𝐶) = (𝐵 ·s 𝐶) ↔ 𝐴 = 𝐵)) | 
| 27 | 8 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 0s <s 𝐶) → 𝐴 ∈  No
) | 
| 28 | 10 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 0s <s 𝐶) → 𝐵 ∈  No
) | 
| 29 | 1 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 0s <s 𝐶) → 𝐶 ∈  No
) | 
| 30 |  | simpr 484 | . . 3
⊢ ((𝜑 ∧ 0s <s 𝐶) → 0s <s
𝐶) | 
| 31 | 27, 28, 29, 30 | mulscan2dlem 28204 | . 2
⊢ ((𝜑 ∧ 0s <s 𝐶) → ((𝐴 ·s 𝐶) = (𝐵 ·s 𝐶) ↔ 𝐴 = 𝐵)) | 
| 32 |  | mulscan2d.4 | . . 3
⊢ (𝜑 → 𝐶 ≠ 0s ) | 
| 33 |  | slttrine 27796 | . . . 4
⊢ ((𝐶 ∈ 
No  ∧ 0s ∈  No ) →
(𝐶 ≠ 0s
↔ (𝐶 <s
0s ∨ 0s <s 𝐶))) | 
| 34 | 1, 2, 33 | sylancl 586 | . . 3
⊢ (𝜑 → (𝐶 ≠ 0s ↔ (𝐶 <s 0s ∨
0s <s 𝐶))) | 
| 35 | 32, 34 | mpbid 232 | . 2
⊢ (𝜑 → (𝐶 <s 0s ∨ 0s
<s 𝐶)) | 
| 36 | 26, 31, 35 | mpjaodan 961 | 1
⊢ (𝜑 → ((𝐴 ·s 𝐶) = (𝐵 ·s 𝐶) ↔ 𝐴 = 𝐵)) |