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	⊢ 𝐴 ∈ ℝ
	problem5.2	⊢ ( ( 2 · 𝐴 ) + 3 ) < 9
Assertion	problem5	⊢ 𝐴 < 3

Proof

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