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

Proof

Step Hyp Ref Expression
1 problem5.1 A
2 problem5.2 2 A + 3 < 9
3 2re 2
4 3 1 remulcli 2 A
5 3re 3
6 9re 9
7 4 5 6 ltaddsubi 2 A + 3 < 9 2 A < 9 3
8 2 7 mpbi 2 A < 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 A < 6
18 6re 6
19 2nn 2
20 19 nngt0i 0 < 2
21 4 18 3 20 ltdiv1ii 2 A < 6 2 A 2 < 6 2
22 17 21 mpbi 2 A 2 < 6 2
23 1 recni A
24 2cn 2
25 2ne0 2 0
26 23 24 25 divcan3i 2 A 2 = A
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 A < 3