# Metamath Proof Explorer

## Theorem problem5

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 ${⊢}{A}\in ℝ$
problem5.2 ${⊢}2{A}+3<9$
Assertion problem5 ${⊢}{A}<3$

### Proof

Step Hyp Ref Expression
1 problem5.1 ${⊢}{A}\in ℝ$
2 problem5.2 ${⊢}2{A}+3<9$
3 2re ${⊢}2\in ℝ$
4 3 1 remulcli ${⊢}2{A}\in ℝ$
5 3re ${⊢}3\in ℝ$
6 9re ${⊢}9\in ℝ$
7 4 5 6 ltaddsubi ${⊢}2{A}+3<9↔2{A}<9-3$
8 2 7 mpbi ${⊢}2{A}<9-3$
9 3cn ${⊢}3\in ℂ$
10 6cn ${⊢}6\in ℂ$
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{A}<6$
18 6re ${⊢}6\in ℝ$
19 2nn ${⊢}2\in ℕ$
20 19 nngt0i ${⊢}0<2$
21 4 18 3 20 ltdiv1ii ${⊢}2{A}<6↔\frac{2{A}}{2}<\frac{6}{2}$
22 17 21 mpbi ${⊢}\frac{2{A}}{2}<\frac{6}{2}$
23 1 recni ${⊢}{A}\in ℂ$
24 2cn ${⊢}2\in ℂ$
25 2ne0 ${⊢}2\ne 0$
26 23 24 25 divcan3i ${⊢}\frac{2{A}}{2}={A}$
27 24 9 mulcomi ${⊢}2\cdot 3=3\cdot 2$
28 3t2e6 ${⊢}3\cdot 2=6$
29 27 28 eqtri ${⊢}2\cdot 3=6$
30 10 24 9 25 divmuli ${⊢}\frac{6}{2}=3↔2\cdot 3=6$
31 29 30 mpbir ${⊢}\frac{6}{2}=3$
32 22 26 31 3brtr3i ${⊢}{A}<3$