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 e. RR
	problem5.2	|- ( ( 2 x. A ) + 3 ) < 9
Assertion	problem5	|- A < 3

Proof

Step	Hyp	Ref	Expression
1		problem5.1	|- A e. RR
2		problem5.2	|- ( ( 2 x. A ) + 3 ) < 9
3		2re	|- 2 e. RR
4	3 1	remulcli	|- ( 2 x. A ) e. RR
5		3re	|- 3 e. RR
6		9re	|- 9 e. RR
7	4 5 6	ltaddsubi	|- ( ( ( 2 x. A ) + 3 ) < 9 <-> ( 2 x. A ) < ( 9 - 3 ) )
8	2 7	mpbi	|- ( 2 x. A ) < ( 9 - 3 )
9		3cn	|- 3 e. CC
10		6cn	|- 6 e. CC
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 x. A ) < 6
18		6re	|- 6 e. RR
19		2nn	|- 2 e. NN
20	19	nngt0i	|- 0 < 2
21	4 18 3 20	ltdiv1ii	|- ( ( 2 x. A ) < 6 <-> ( ( 2 x. A ) / 2 ) < ( 6 / 2 ) )
22	17 21	mpbi	|- ( ( 2 x. A ) / 2 ) < ( 6 / 2 )
23	1	recni	|- A e. CC
24		2cn	|- 2 e. CC
25		2ne0	|- 2 =/= 0
26	23 24 25	divcan3i	|- ( ( 2 x. A ) / 2 ) = A
27	24 9	mulcomi	|- ( 2 x. 3 ) = ( 3 x. 2 )
28		3t2e6	|- ( 3 x. 2 ) = 6
29	27 28	eqtri	|- ( 2 x. 3 ) = 6
30	10 24 9 25	divmuli	|- ( ( 6 / 2 ) = 3 <-> ( 2 x. 3 ) = 6 )
31	29 30	mpbir	|- ( 6 / 2 ) = 3
32	22 26 31	3brtr3i	|- A < 3