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 𝐴 ∈ ℝ
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