Proof of Theorem addltmul
Step | Hyp | Ref
| Expression |
1 | | 2re 11449 |
. . . . . . 7
⊢ 2 ∈
ℝ |
2 | | 1re 10376 |
. . . . . . 7
⊢ 1 ∈
ℝ |
3 | | ltsub1 10871 |
. . . . . . 7
⊢ ((2
∈ ℝ ∧ 𝐴
∈ ℝ ∧ 1 ∈ ℝ) → (2 < 𝐴 ↔ (2 − 1) < (𝐴 − 1))) |
4 | 1, 2, 3 | mp3an13 1525 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → (2 <
𝐴 ↔ (2 − 1) <
(𝐴 −
1))) |
5 | | 2m1e1 11508 |
. . . . . . 7
⊢ (2
− 1) = 1 |
6 | 5 | breq1i 4893 |
. . . . . 6
⊢ ((2
− 1) < (𝐴 −
1) ↔ 1 < (𝐴 −
1)) |
7 | 4, 6 | syl6bb 279 |
. . . . 5
⊢ (𝐴 ∈ ℝ → (2 <
𝐴 ↔ 1 < (𝐴 − 1))) |
8 | | ltsub1 10871 |
. . . . . . 7
⊢ ((2
∈ ℝ ∧ 𝐵
∈ ℝ ∧ 1 ∈ ℝ) → (2 < 𝐵 ↔ (2 − 1) < (𝐵 − 1))) |
9 | 1, 2, 8 | mp3an13 1525 |
. . . . . 6
⊢ (𝐵 ∈ ℝ → (2 <
𝐵 ↔ (2 − 1) <
(𝐵 −
1))) |
10 | 5 | breq1i 4893 |
. . . . . 6
⊢ ((2
− 1) < (𝐵 −
1) ↔ 1 < (𝐵 −
1)) |
11 | 9, 10 | syl6bb 279 |
. . . . 5
⊢ (𝐵 ∈ ℝ → (2 <
𝐵 ↔ 1 < (𝐵 − 1))) |
12 | 7, 11 | bi2anan9 629 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((2 <
𝐴 ∧ 2 < 𝐵) ↔ (1 < (𝐴 − 1) ∧ 1 < (𝐵 − 1)))) |
13 | | peano2rem 10690 |
. . . . 5
⊢ (𝐴 ∈ ℝ → (𝐴 − 1) ∈
ℝ) |
14 | | peano2rem 10690 |
. . . . 5
⊢ (𝐵 ∈ ℝ → (𝐵 − 1) ∈
ℝ) |
15 | | mulgt1 11236 |
. . . . . 6
⊢ ((((𝐴 − 1) ∈ ℝ ∧
(𝐵 − 1) ∈
ℝ) ∧ (1 < (𝐴
− 1) ∧ 1 < (𝐵
− 1))) → 1 < ((𝐴 − 1) · (𝐵 − 1))) |
16 | 15 | ex 403 |
. . . . 5
⊢ (((𝐴 − 1) ∈ ℝ ∧
(𝐵 − 1) ∈
ℝ) → ((1 < (𝐴
− 1) ∧ 1 < (𝐵
− 1)) → 1 < ((𝐴 − 1) · (𝐵 − 1)))) |
17 | 13, 14, 16 | syl2an 589 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((1 <
(𝐴 − 1) ∧ 1 <
(𝐵 − 1)) → 1
< ((𝐴 − 1)
· (𝐵 −
1)))) |
18 | 12, 17 | sylbid 232 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((2 <
𝐴 ∧ 2 < 𝐵) → 1 < ((𝐴 − 1) · (𝐵 − 1)))) |
19 | | recn 10362 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
20 | | recn 10362 |
. . . . . 6
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℂ) |
21 | | ax-1cn 10330 |
. . . . . . 7
⊢ 1 ∈
ℂ |
22 | | mulsub 10818 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) ∧ (𝐵 ∈
ℂ ∧ 1 ∈ ℂ)) → ((𝐴 − 1) · (𝐵 − 1)) = (((𝐴 · 𝐵) + (1 · 1)) − ((𝐴 · 1) + (𝐵 · 1)))) |
23 | 21, 22 | mpanl2 691 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 1 ∈
ℂ)) → ((𝐴
− 1) · (𝐵
− 1)) = (((𝐴 ·
𝐵) + (1 · 1))
− ((𝐴 · 1) +
(𝐵 ·
1)))) |
24 | 21, 23 | mpanr2 694 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 1) · (𝐵 − 1)) = (((𝐴 · 𝐵) + (1 · 1)) − ((𝐴 · 1) + (𝐵 · 1)))) |
25 | 19, 20, 24 | syl2an 589 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 − 1) · (𝐵 − 1)) = (((𝐴 · 𝐵) + (1 · 1)) − ((𝐴 · 1) + (𝐵 · 1)))) |
26 | 25 | breq2d 4898 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (1 <
((𝐴 − 1) ·
(𝐵 − 1)) ↔ 1
< (((𝐴 · 𝐵) + (1 · 1)) −
((𝐴 · 1) + (𝐵 ·
1))))) |
27 | | 1t1e1 11544 |
. . . . . . 7
⊢ (1
· 1) = 1 |
28 | 27 | oveq2i 6933 |
. . . . . 6
⊢ ((𝐴 · 𝐵) + (1 · 1)) = ((𝐴 · 𝐵) + 1) |
29 | 28 | breq2i 4894 |
. . . . 5
⊢ ((((𝐴 · 1) + (𝐵 · 1)) + 1) < ((𝐴 · 𝐵) + (1 · 1)) ↔ (((𝐴 · 1) + (𝐵 · 1)) + 1) < ((𝐴 · 𝐵) + 1)) |
30 | | remulcl 10357 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 1 ∈
ℝ) → (𝐴 ·
1) ∈ ℝ) |
31 | 2, 30 | mpan2 681 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → (𝐴 · 1) ∈
ℝ) |
32 | | remulcl 10357 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ ∧ 1 ∈
ℝ) → (𝐵 ·
1) ∈ ℝ) |
33 | 2, 32 | mpan2 681 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ → (𝐵 · 1) ∈
ℝ) |
34 | | readdcl 10355 |
. . . . . . 7
⊢ (((𝐴 · 1) ∈ ℝ
∧ (𝐵 · 1) ∈
ℝ) → ((𝐴
· 1) + (𝐵 ·
1)) ∈ ℝ) |
35 | 31, 33, 34 | syl2an 589 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 · 1) + (𝐵 · 1)) ∈
ℝ) |
36 | | remulcl 10357 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ) |
37 | 2, 2 | remulcli 10393 |
. . . . . . 7
⊢ (1
· 1) ∈ ℝ |
38 | | readdcl 10355 |
. . . . . . 7
⊢ (((𝐴 · 𝐵) ∈ ℝ ∧ (1 · 1) ∈
ℝ) → ((𝐴
· 𝐵) + (1 ·
1)) ∈ ℝ) |
39 | 36, 37, 38 | sylancl 580 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 · 𝐵) + (1 · 1)) ∈
ℝ) |
40 | | ltaddsub2 10850 |
. . . . . . 7
⊢ ((((𝐴 · 1) + (𝐵 · 1)) ∈ ℝ
∧ 1 ∈ ℝ ∧ ((𝐴 · 𝐵) + (1 · 1)) ∈ ℝ) →
((((𝐴 · 1) + (𝐵 · 1)) + 1) < ((𝐴 · 𝐵) + (1 · 1)) ↔ 1 < (((𝐴 · 𝐵) + (1 · 1)) − ((𝐴 · 1) + (𝐵 ·
1))))) |
41 | 2, 40 | mp3an2 1522 |
. . . . . 6
⊢ ((((𝐴 · 1) + (𝐵 · 1)) ∈ ℝ
∧ ((𝐴 · 𝐵) + (1 · 1)) ∈
ℝ) → ((((𝐴
· 1) + (𝐵 ·
1)) + 1) < ((𝐴 ·
𝐵) + (1 · 1)) ↔
1 < (((𝐴 · 𝐵) + (1 · 1)) −
((𝐴 · 1) + (𝐵 ·
1))))) |
42 | 35, 39, 41 | syl2anc 579 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((((𝐴 · 1) + (𝐵 · 1)) + 1) < ((𝐴 · 𝐵) + (1 · 1)) ↔ 1 < (((𝐴 · 𝐵) + (1 · 1)) − ((𝐴 · 1) + (𝐵 ·
1))))) |
43 | 29, 42 | syl5rbbr 278 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (1 <
(((𝐴 · 𝐵) + (1 · 1)) −
((𝐴 · 1) + (𝐵 · 1))) ↔ (((𝐴 · 1) + (𝐵 · 1)) + 1) < ((𝐴 · 𝐵) + 1))) |
44 | | ltadd1 10842 |
. . . . . . 7
⊢ ((((𝐴 · 1) + (𝐵 · 1)) ∈ ℝ
∧ (𝐴 · 𝐵) ∈ ℝ ∧ 1 ∈
ℝ) → (((𝐴
· 1) + (𝐵 ·
1)) < (𝐴 · 𝐵) ↔ (((𝐴 · 1) + (𝐵 · 1)) + 1) < ((𝐴 · 𝐵) + 1))) |
45 | 2, 44 | mp3an3 1523 |
. . . . . 6
⊢ ((((𝐴 · 1) + (𝐵 · 1)) ∈ ℝ
∧ (𝐴 · 𝐵) ∈ ℝ) →
(((𝐴 · 1) + (𝐵 · 1)) < (𝐴 · 𝐵) ↔ (((𝐴 · 1) + (𝐵 · 1)) + 1) < ((𝐴 · 𝐵) + 1))) |
46 | 35, 36, 45 | syl2anc 579 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (((𝐴 · 1) + (𝐵 · 1)) < (𝐴 · 𝐵) ↔ (((𝐴 · 1) + (𝐵 · 1)) + 1) < ((𝐴 · 𝐵) + 1))) |
47 | | ax-1rid 10342 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴) |
48 | | ax-1rid 10342 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ → (𝐵 · 1) = 𝐵) |
49 | 47, 48 | oveqan12d 6941 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 · 1) + (𝐵 · 1)) = (𝐴 + 𝐵)) |
50 | 49 | breq1d 4896 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (((𝐴 · 1) + (𝐵 · 1)) < (𝐴 · 𝐵) ↔ (𝐴 + 𝐵) < (𝐴 · 𝐵))) |
51 | 46, 50 | bitr3d 273 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((((𝐴 · 1) + (𝐵 · 1)) + 1) < ((𝐴 · 𝐵) + 1) ↔ (𝐴 + 𝐵) < (𝐴 · 𝐵))) |
52 | 26, 43, 51 | 3bitrd 297 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (1 <
((𝐴 − 1) ·
(𝐵 − 1)) ↔
(𝐴 + 𝐵) < (𝐴 · 𝐵))) |
53 | 18, 52 | sylibd 231 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((2 <
𝐴 ∧ 2 < 𝐵) → (𝐴 + 𝐵) < (𝐴 · 𝐵))) |
54 | 53 | imp 397 |
1
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (2 <
𝐴 ∧ 2 < 𝐵)) → (𝐴 + 𝐵) < (𝐴 · 𝐵)) |