Proof of Theorem slemuld
Step | Hyp | Ref
| Expression |
1 | | slemuld.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ No
) |
2 | | slemuld.4 |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ No
) |
3 | 1, 2 | mulscld 27520 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ·s 𝐷) ∈ No
) |
4 | | slemuld.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ No
) |
5 | 1, 4 | mulscld 27520 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ·s 𝐶) ∈ No
) |
6 | 3, 5 | subscld 27464 |
. . . . . 6
⊢ (𝜑 → ((𝐴 ·s 𝐷) -s (𝐴 ·s 𝐶)) ∈ No
) |
7 | 6 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴 <s 𝐵 ∧ 𝐶 <s 𝐷)) → ((𝐴 ·s 𝐷) -s (𝐴 ·s 𝐶)) ∈ No
) |
8 | | slemuld.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ No
) |
9 | 8, 2 | mulscld 27520 |
. . . . . . 7
⊢ (𝜑 → (𝐵 ·s 𝐷) ∈ No
) |
10 | 8, 4 | mulscld 27520 |
. . . . . . 7
⊢ (𝜑 → (𝐵 ·s 𝐶) ∈ No
) |
11 | 9, 10 | subscld 27464 |
. . . . . 6
⊢ (𝜑 → ((𝐵 ·s 𝐷) -s (𝐵 ·s 𝐶)) ∈ No
) |
12 | 11 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴 <s 𝐵 ∧ 𝐶 <s 𝐷)) → ((𝐵 ·s 𝐷) -s (𝐵 ·s 𝐶)) ∈ No
) |
13 | 1 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐴 <s 𝐵 ∧ 𝐶 <s 𝐷)) → 𝐴 ∈ No
) |
14 | 8 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐴 <s 𝐵 ∧ 𝐶 <s 𝐷)) → 𝐵 ∈ No
) |
15 | 4 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐴 <s 𝐵 ∧ 𝐶 <s 𝐷)) → 𝐶 ∈ No
) |
16 | 2 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐴 <s 𝐵 ∧ 𝐶 <s 𝐷)) → 𝐷 ∈ No
) |
17 | | simprl 769 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐴 <s 𝐵 ∧ 𝐶 <s 𝐷)) → 𝐴 <s 𝐵) |
18 | | simprr 771 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐴 <s 𝐵 ∧ 𝐶 <s 𝐷)) → 𝐶 <s 𝐷) |
19 | 13, 14, 15, 16, 17, 18 | sltmuld 27522 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴 <s 𝐵 ∧ 𝐶 <s 𝐷)) → ((𝐴 ·s 𝐷) -s (𝐴 ·s 𝐶)) <s ((𝐵 ·s 𝐷) -s (𝐵 ·s 𝐶))) |
20 | 7, 12, 19 | sltled 27201 |
. . . 4
⊢ ((𝜑 ∧ (𝐴 <s 𝐵 ∧ 𝐶 <s 𝐷)) → ((𝐴 ·s 𝐷) -s (𝐴 ·s 𝐶)) ≤s ((𝐵 ·s 𝐷) -s (𝐵 ·s 𝐶))) |
21 | 20 | anassrs 468 |
. . 3
⊢ (((𝜑 ∧ 𝐴 <s 𝐵) ∧ 𝐶 <s 𝐷) → ((𝐴 ·s 𝐷) -s (𝐴 ·s 𝐶)) ≤s ((𝐵 ·s 𝐷) -s (𝐵 ·s 𝐶))) |
22 | | 0sno 27256 |
. . . . . . . 8
⊢
0s ∈ No |
23 | | slerflex 27195 |
. . . . . . . 8
⊢ (
0s ∈ No → 0s
≤s 0s ) |
24 | 22, 23 | mp1i 13 |
. . . . . . 7
⊢ (𝜑 → 0s ≤s
0s ) |
25 | | subsid 27466 |
. . . . . . . 8
⊢ ((𝐴 ·s 𝐷) ∈
No → ((𝐴
·s 𝐷)
-s (𝐴
·s 𝐷)) =
0s ) |
26 | 3, 25 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 ·s 𝐷) -s (𝐴 ·s 𝐷)) = 0s ) |
27 | | subsid 27466 |
. . . . . . . 8
⊢ ((𝐵 ·s 𝐷) ∈
No → ((𝐵
·s 𝐷)
-s (𝐵
·s 𝐷)) =
0s ) |
28 | 9, 27 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝐵 ·s 𝐷) -s (𝐵 ·s 𝐷)) = 0s ) |
29 | 24, 26, 28 | 3brtr4d 5174 |
. . . . . 6
⊢ (𝜑 → ((𝐴 ·s 𝐷) -s (𝐴 ·s 𝐷)) ≤s ((𝐵 ·s 𝐷) -s (𝐵 ·s 𝐷))) |
30 | | oveq2 7402 |
. . . . . . . 8
⊢ (𝐶 = 𝐷 → (𝐴 ·s 𝐶) = (𝐴 ·s 𝐷)) |
31 | 30 | oveq2d 7410 |
. . . . . . 7
⊢ (𝐶 = 𝐷 → ((𝐴 ·s 𝐷) -s (𝐴 ·s 𝐶)) = ((𝐴 ·s 𝐷) -s (𝐴 ·s 𝐷))) |
32 | | oveq2 7402 |
. . . . . . . 8
⊢ (𝐶 = 𝐷 → (𝐵 ·s 𝐶) = (𝐵 ·s 𝐷)) |
33 | 32 | oveq2d 7410 |
. . . . . . 7
⊢ (𝐶 = 𝐷 → ((𝐵 ·s 𝐷) -s (𝐵 ·s 𝐶)) = ((𝐵 ·s 𝐷) -s (𝐵 ·s 𝐷))) |
34 | 31, 33 | breq12d 5155 |
. . . . . 6
⊢ (𝐶 = 𝐷 → (((𝐴 ·s 𝐷) -s (𝐴 ·s 𝐶)) ≤s ((𝐵 ·s 𝐷) -s (𝐵 ·s 𝐶)) ↔ ((𝐴 ·s 𝐷) -s (𝐴 ·s 𝐷)) ≤s ((𝐵 ·s 𝐷) -s (𝐵 ·s 𝐷)))) |
35 | 29, 34 | syl5ibrcom 246 |
. . . . 5
⊢ (𝜑 → (𝐶 = 𝐷 → ((𝐴 ·s 𝐷) -s (𝐴 ·s 𝐶)) ≤s ((𝐵 ·s 𝐷) -s (𝐵 ·s 𝐶)))) |
36 | 35 | imp 407 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 = 𝐷) → ((𝐴 ·s 𝐷) -s (𝐴 ·s 𝐶)) ≤s ((𝐵 ·s 𝐷) -s (𝐵 ·s 𝐶))) |
37 | 36 | adantlr 713 |
. . 3
⊢ (((𝜑 ∧ 𝐴 <s 𝐵) ∧ 𝐶 = 𝐷) → ((𝐴 ·s 𝐷) -s (𝐴 ·s 𝐶)) ≤s ((𝐵 ·s 𝐷) -s (𝐵 ·s 𝐶))) |
38 | | slemuld.6 |
. . . . 5
⊢ (𝜑 → 𝐶 ≤s 𝐷) |
39 | | sleloe 27186 |
. . . . . 6
⊢ ((𝐶 ∈
No ∧ 𝐷 ∈
No ) → (𝐶 ≤s 𝐷 ↔ (𝐶 <s 𝐷 ∨ 𝐶 = 𝐷))) |
40 | 4, 2, 39 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝐶 ≤s 𝐷 ↔ (𝐶 <s 𝐷 ∨ 𝐶 = 𝐷))) |
41 | 38, 40 | mpbid 231 |
. . . 4
⊢ (𝜑 → (𝐶 <s 𝐷 ∨ 𝐶 = 𝐷)) |
42 | 41 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝐴 <s 𝐵) → (𝐶 <s 𝐷 ∨ 𝐶 = 𝐷)) |
43 | 21, 37, 42 | mpjaodan 957 |
. 2
⊢ ((𝜑 ∧ 𝐴 <s 𝐵) → ((𝐴 ·s 𝐷) -s (𝐴 ·s 𝐶)) ≤s ((𝐵 ·s 𝐷) -s (𝐵 ·s 𝐶))) |
44 | | slerflex 27195 |
. . . . 5
⊢ (((𝐵 ·s 𝐷) -s (𝐵 ·s 𝐶)) ∈
No → ((𝐵
·s 𝐷)
-s (𝐵
·s 𝐶))
≤s ((𝐵
·s 𝐷)
-s (𝐵
·s 𝐶))) |
45 | 11, 44 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝐵 ·s 𝐷) -s (𝐵 ·s 𝐶)) ≤s ((𝐵 ·s 𝐷) -s (𝐵 ·s 𝐶))) |
46 | | oveq1 7401 |
. . . . . 6
⊢ (𝐴 = 𝐵 → (𝐴 ·s 𝐷) = (𝐵 ·s 𝐷)) |
47 | | oveq1 7401 |
. . . . . 6
⊢ (𝐴 = 𝐵 → (𝐴 ·s 𝐶) = (𝐵 ·s 𝐶)) |
48 | 46, 47 | oveq12d 7412 |
. . . . 5
⊢ (𝐴 = 𝐵 → ((𝐴 ·s 𝐷) -s (𝐴 ·s 𝐶)) = ((𝐵 ·s 𝐷) -s (𝐵 ·s 𝐶))) |
49 | 48 | breq1d 5152 |
. . . 4
⊢ (𝐴 = 𝐵 → (((𝐴 ·s 𝐷) -s (𝐴 ·s 𝐶)) ≤s ((𝐵 ·s 𝐷) -s (𝐵 ·s 𝐶)) ↔ ((𝐵 ·s 𝐷) -s (𝐵 ·s 𝐶)) ≤s ((𝐵 ·s 𝐷) -s (𝐵 ·s 𝐶)))) |
50 | 45, 49 | syl5ibrcom 246 |
. . 3
⊢ (𝜑 → (𝐴 = 𝐵 → ((𝐴 ·s 𝐷) -s (𝐴 ·s 𝐶)) ≤s ((𝐵 ·s 𝐷) -s (𝐵 ·s 𝐶)))) |
51 | 50 | imp 407 |
. 2
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → ((𝐴 ·s 𝐷) -s (𝐴 ·s 𝐶)) ≤s ((𝐵 ·s 𝐷) -s (𝐵 ·s 𝐶))) |
52 | | slemuld.5 |
. . 3
⊢ (𝜑 → 𝐴 ≤s 𝐵) |
53 | | sleloe 27186 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 ≤s 𝐵 ↔ (𝐴 <s 𝐵 ∨ 𝐴 = 𝐵))) |
54 | 1, 8, 53 | syl2anc 584 |
. . 3
⊢ (𝜑 → (𝐴 ≤s 𝐵 ↔ (𝐴 <s 𝐵 ∨ 𝐴 = 𝐵))) |
55 | 52, 54 | mpbid 231 |
. 2
⊢ (𝜑 → (𝐴 <s 𝐵 ∨ 𝐴 = 𝐵)) |
56 | 43, 51, 55 | mpjaodan 957 |
1
⊢ (𝜑 → ((𝐴 ·s 𝐷) -s (𝐴 ·s 𝐶)) ≤s ((𝐵 ·s 𝐷) -s (𝐵 ·s 𝐶))) |