Step | Hyp | Ref
| Expression |
1 | | ltmul1a 8483 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) ∧ 𝐴 < 𝐵) → (𝐴 · 𝐶) < (𝐵 · 𝐶)) |
2 | 1 | ex 114 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) → (𝐴 < 𝐵 → (𝐴 · 𝐶) < (𝐵 · 𝐶))) |
3 | | recexgt0 8472 |
. . . 4
⊢ ((𝐶 ∈ ℝ ∧ 0 <
𝐶) → ∃𝑥 ∈ ℝ (0 < 𝑥 ∧ (𝐶 · 𝑥) = 1)) |
4 | 3 | 3ad2ant3 1009 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) → ∃𝑥 ∈ ℝ (0 < 𝑥 ∧ (𝐶 · 𝑥) = 1)) |
5 | | simpl1 989 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) ∧ (𝑥 ∈ ℝ ∧ (0 <
𝑥 ∧ (𝐶 · 𝑥) = 1))) → 𝐴 ∈ ℝ) |
6 | | simpl3l 1041 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) ∧ (𝑥 ∈ ℝ ∧ (0 <
𝑥 ∧ (𝐶 · 𝑥) = 1))) → 𝐶 ∈ ℝ) |
7 | 5, 6 | remulcld 7923 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) ∧ (𝑥 ∈ ℝ ∧ (0 <
𝑥 ∧ (𝐶 · 𝑥) = 1))) → (𝐴 · 𝐶) ∈ ℝ) |
8 | | simpl2 990 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) ∧ (𝑥 ∈ ℝ ∧ (0 <
𝑥 ∧ (𝐶 · 𝑥) = 1))) → 𝐵 ∈ ℝ) |
9 | 8, 6 | remulcld 7923 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) ∧ (𝑥 ∈ ℝ ∧ (0 <
𝑥 ∧ (𝐶 · 𝑥) = 1))) → (𝐵 · 𝐶) ∈ ℝ) |
10 | | simprl 521 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) ∧ (𝑥 ∈ ℝ ∧ (0 <
𝑥 ∧ (𝐶 · 𝑥) = 1))) → 𝑥 ∈ ℝ) |
11 | | simprrl 529 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) ∧ (𝑥 ∈ ℝ ∧ (0 <
𝑥 ∧ (𝐶 · 𝑥) = 1))) → 0 < 𝑥) |
12 | 10, 11 | jca 304 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) ∧ (𝑥 ∈ ℝ ∧ (0 <
𝑥 ∧ (𝐶 · 𝑥) = 1))) → (𝑥 ∈ ℝ ∧ 0 < 𝑥)) |
13 | 7, 9, 12 | 3jca 1166 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) ∧ (𝑥 ∈ ℝ ∧ (0 <
𝑥 ∧ (𝐶 · 𝑥) = 1))) → ((𝐴 · 𝐶) ∈ ℝ ∧ (𝐵 · 𝐶) ∈ ℝ ∧ (𝑥 ∈ ℝ ∧ 0 < 𝑥))) |
14 | | ltmul1a 8483 |
. . . . . . . 8
⊢ ((((𝐴 · 𝐶) ∈ ℝ ∧ (𝐵 · 𝐶) ∈ ℝ ∧ (𝑥 ∈ ℝ ∧ 0 < 𝑥)) ∧ (𝐴 · 𝐶) < (𝐵 · 𝐶)) → ((𝐴 · 𝐶) · 𝑥) < ((𝐵 · 𝐶) · 𝑥)) |
15 | 13, 14 | sylan 281 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) ∧ (𝑥 ∈ ℝ ∧ (0 <
𝑥 ∧ (𝐶 · 𝑥) = 1))) ∧ (𝐴 · 𝐶) < (𝐵 · 𝐶)) → ((𝐴 · 𝐶) · 𝑥) < ((𝐵 · 𝐶) · 𝑥)) |
16 | 5 | recnd 7921 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) ∧ (𝑥 ∈ ℝ ∧ (0 <
𝑥 ∧ (𝐶 · 𝑥) = 1))) → 𝐴 ∈ ℂ) |
17 | 16 | adantr 274 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) ∧ (𝑥 ∈ ℝ ∧ (0 <
𝑥 ∧ (𝐶 · 𝑥) = 1))) ∧ (𝐴 · 𝐶) < (𝐵 · 𝐶)) → 𝐴 ∈ ℂ) |
18 | 6 | recnd 7921 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) ∧ (𝑥 ∈ ℝ ∧ (0 <
𝑥 ∧ (𝐶 · 𝑥) = 1))) → 𝐶 ∈ ℂ) |
19 | 18 | adantr 274 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) ∧ (𝑥 ∈ ℝ ∧ (0 <
𝑥 ∧ (𝐶 · 𝑥) = 1))) ∧ (𝐴 · 𝐶) < (𝐵 · 𝐶)) → 𝐶 ∈ ℂ) |
20 | 10 | recnd 7921 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) ∧ (𝑥 ∈ ℝ ∧ (0 <
𝑥 ∧ (𝐶 · 𝑥) = 1))) → 𝑥 ∈ ℂ) |
21 | 20 | adantr 274 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) ∧ (𝑥 ∈ ℝ ∧ (0 <
𝑥 ∧ (𝐶 · 𝑥) = 1))) ∧ (𝐴 · 𝐶) < (𝐵 · 𝐶)) → 𝑥 ∈ ℂ) |
22 | 17, 19, 21 | mulassd 7916 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) ∧ (𝑥 ∈ ℝ ∧ (0 <
𝑥 ∧ (𝐶 · 𝑥) = 1))) ∧ (𝐴 · 𝐶) < (𝐵 · 𝐶)) → ((𝐴 · 𝐶) · 𝑥) = (𝐴 · (𝐶 · 𝑥))) |
23 | 8 | recnd 7921 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) ∧ (𝑥 ∈ ℝ ∧ (0 <
𝑥 ∧ (𝐶 · 𝑥) = 1))) → 𝐵 ∈ ℂ) |
24 | 23 | adantr 274 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) ∧ (𝑥 ∈ ℝ ∧ (0 <
𝑥 ∧ (𝐶 · 𝑥) = 1))) ∧ (𝐴 · 𝐶) < (𝐵 · 𝐶)) → 𝐵 ∈ ℂ) |
25 | 24, 19, 21 | mulassd 7916 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) ∧ (𝑥 ∈ ℝ ∧ (0 <
𝑥 ∧ (𝐶 · 𝑥) = 1))) ∧ (𝐴 · 𝐶) < (𝐵 · 𝐶)) → ((𝐵 · 𝐶) · 𝑥) = (𝐵 · (𝐶 · 𝑥))) |
26 | 15, 22, 25 | 3brtr3d 4010 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) ∧ (𝑥 ∈ ℝ ∧ (0 <
𝑥 ∧ (𝐶 · 𝑥) = 1))) ∧ (𝐴 · 𝐶) < (𝐵 · 𝐶)) → (𝐴 · (𝐶 · 𝑥)) < (𝐵 · (𝐶 · 𝑥))) |
27 | | simprrr 530 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) ∧ (𝑥 ∈ ℝ ∧ (0 <
𝑥 ∧ (𝐶 · 𝑥) = 1))) → (𝐶 · 𝑥) = 1) |
28 | 27 | adantr 274 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) ∧ (𝑥 ∈ ℝ ∧ (0 <
𝑥 ∧ (𝐶 · 𝑥) = 1))) ∧ (𝐴 · 𝐶) < (𝐵 · 𝐶)) → (𝐶 · 𝑥) = 1) |
29 | 28 | oveq2d 5855 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) ∧ (𝑥 ∈ ℝ ∧ (0 <
𝑥 ∧ (𝐶 · 𝑥) = 1))) ∧ (𝐴 · 𝐶) < (𝐵 · 𝐶)) → (𝐴 · (𝐶 · 𝑥)) = (𝐴 · 1)) |
30 | 28 | oveq2d 5855 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) ∧ (𝑥 ∈ ℝ ∧ (0 <
𝑥 ∧ (𝐶 · 𝑥) = 1))) ∧ (𝐴 · 𝐶) < (𝐵 · 𝐶)) → (𝐵 · (𝐶 · 𝑥)) = (𝐵 · 1)) |
31 | 26, 29, 30 | 3brtr3d 4010 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) ∧ (𝑥 ∈ ℝ ∧ (0 <
𝑥 ∧ (𝐶 · 𝑥) = 1))) ∧ (𝐴 · 𝐶) < (𝐵 · 𝐶)) → (𝐴 · 1) < (𝐵 · 1)) |
32 | 17 | mulid1d 7910 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) ∧ (𝑥 ∈ ℝ ∧ (0 <
𝑥 ∧ (𝐶 · 𝑥) = 1))) ∧ (𝐴 · 𝐶) < (𝐵 · 𝐶)) → (𝐴 · 1) = 𝐴) |
33 | 24 | mulid1d 7910 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) ∧ (𝑥 ∈ ℝ ∧ (0 <
𝑥 ∧ (𝐶 · 𝑥) = 1))) ∧ (𝐴 · 𝐶) < (𝐵 · 𝐶)) → (𝐵 · 1) = 𝐵) |
34 | 31, 32, 33 | 3brtr3d 4010 |
. . . 4
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) ∧ (𝑥 ∈ ℝ ∧ (0 <
𝑥 ∧ (𝐶 · 𝑥) = 1))) ∧ (𝐴 · 𝐶) < (𝐵 · 𝐶)) → 𝐴 < 𝐵) |
35 | 34 | ex 114 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) ∧ (𝑥 ∈ ℝ ∧ (0 <
𝑥 ∧ (𝐶 · 𝑥) = 1))) → ((𝐴 · 𝐶) < (𝐵 · 𝐶) → 𝐴 < 𝐵)) |
36 | 4, 35 | rexlimddv 2586 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) → ((𝐴 · 𝐶) < (𝐵 · 𝐶) → 𝐴 < 𝐵)) |
37 | 2, 36 | impbid 128 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) → (𝐴 < 𝐵 ↔ (𝐴 · 𝐶) < (𝐵 · 𝐶))) |