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	$$⊢2A+3<9$$
Assertion	problem5	$$⊢A<3$$

Proof

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