Description: Practice problem 5. Clues: 3brtr3i mpbi breqtri ltaddsubi remulcli 2re 3re 9re eqcomi mvlladdi 3cn 6cn eqtr3i 6p3e9 addcomi ltdiv1ii 6re nngt0i 2nn divcan3i recni 2cn 2ne0 mpbir eqtri mulcomi 3t2e6 divmuli . (Contributed by Filip Cernatescu, 16-Mar-2019) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | problem5.1 | ⊢ 𝐴 ∈ ℝ | |
problem5.2 | ⊢ ( ( 2 · 𝐴 ) + 3 ) < 9 | ||
Assertion | problem5 | ⊢ 𝐴 < 3 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | problem5.1 | ⊢ 𝐴 ∈ ℝ | |
2 | problem5.2 | ⊢ ( ( 2 · 𝐴 ) + 3 ) < 9 | |
3 | 2re | ⊢ 2 ∈ ℝ | |
4 | 3 1 | remulcli | ⊢ ( 2 · 𝐴 ) ∈ ℝ |
5 | 3re | ⊢ 3 ∈ ℝ | |
6 | 9re | ⊢ 9 ∈ ℝ | |
7 | 4 5 6 | ltaddsubi | ⊢ ( ( ( 2 · 𝐴 ) + 3 ) < 9 ↔ ( 2 · 𝐴 ) < ( 9 − 3 ) ) |
8 | 2 7 | mpbi | ⊢ ( 2 · 𝐴 ) < ( 9 − 3 ) |
9 | 3cn | ⊢ 3 ∈ ℂ | |
10 | 6cn | ⊢ 6 ∈ ℂ | |
11 | 6p3e9 | ⊢ ( 6 + 3 ) = 9 | |
12 | 10 9 | addcomi | ⊢ ( 6 + 3 ) = ( 3 + 6 ) |
13 | 11 12 | eqtr3i | ⊢ 9 = ( 3 + 6 ) |
14 | 13 | eqcomi | ⊢ ( 3 + 6 ) = 9 |
15 | 9 10 14 | mvlladdi | ⊢ 6 = ( 9 − 3 ) |
16 | 15 | eqcomi | ⊢ ( 9 − 3 ) = 6 |
17 | 8 16 | breqtri | ⊢ ( 2 · 𝐴 ) < 6 |
18 | 6re | ⊢ 6 ∈ ℝ | |
19 | 2nn | ⊢ 2 ∈ ℕ | |
20 | 19 | nngt0i | ⊢ 0 < 2 |
21 | 4 18 3 20 | ltdiv1ii | ⊢ ( ( 2 · 𝐴 ) < 6 ↔ ( ( 2 · 𝐴 ) / 2 ) < ( 6 / 2 ) ) |
22 | 17 21 | mpbi | ⊢ ( ( 2 · 𝐴 ) / 2 ) < ( 6 / 2 ) |
23 | 1 | recni | ⊢ 𝐴 ∈ ℂ |
24 | 2cn | ⊢ 2 ∈ ℂ | |
25 | 2ne0 | ⊢ 2 ≠ 0 | |
26 | 23 24 25 | divcan3i | ⊢ ( ( 2 · 𝐴 ) / 2 ) = 𝐴 |
27 | 24 9 | mulcomi | ⊢ ( 2 · 3 ) = ( 3 · 2 ) |
28 | 3t2e6 | ⊢ ( 3 · 2 ) = 6 | |
29 | 27 28 | eqtri | ⊢ ( 2 · 3 ) = 6 |
30 | 10 24 9 25 | divmuli | ⊢ ( ( 6 / 2 ) = 3 ↔ ( 2 · 3 ) = 6 ) |
31 | 29 30 | mpbir | ⊢ ( 6 / 2 ) = 3 |
32 | 22 26 31 | 3brtr3i | ⊢ 𝐴 < 3 |