This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nn0opthlem1

Description: A rather pretty lemma for nn0opthi . (Contributed by Raph Levien, 10-Dec-2002)

Ref Expression
Hypotheses nn0opthlem1.1 ⊢ 𝐴 ∈ ℕ0
nn0opthlem1.2 ⊢ 𝐶 ∈ ℕ0
Assertion nn0opthlem1 ( 𝐴 < 𝐶 ↔ ( ( 𝐴 · 𝐴 ) + ( 2 · 𝐴 ) ) < ( 𝐶 · 𝐶 ) )

Proof

Step Hyp Ref Expression
1 nn0opthlem1.1 ⊢ 𝐴 ∈ ℕ0
2 nn0opthlem1.2 ⊢ 𝐶 ∈ ℕ0
3 1nn0 ⊢ 1 ∈ ℕ0
4 1 3 nn0addcli ⊢ ( 𝐴 + 1 ) ∈ ℕ0
5 4 2 nn0le2msqi ⊢ ( ( 𝐴 + 1 ) ≤ 𝐶 ↔ ( ( 𝐴 + 1 ) · ( 𝐴 + 1 ) ) ≤ ( 𝐶 · 𝐶 ) )
6 nn0ltp1le ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( 𝐴 < 𝐶 ↔ ( 𝐴 + 1 ) ≤ 𝐶 ) )
7 1 2 6 mp2an ⊢ ( 𝐴 < 𝐶 ↔ ( 𝐴 + 1 ) ≤ 𝐶 )
8 1 1 nn0mulcli ⊢ ( 𝐴 · 𝐴 ) ∈ ℕ0
9 2nn0 ⊢ 2 ∈ ℕ0
10 9 1 nn0mulcli ⊢ ( 2 · 𝐴 ) ∈ ℕ0
11 8 10 nn0addcli ⊢ ( ( 𝐴 · 𝐴 ) + ( 2 · 𝐴 ) ) ∈ ℕ0
12 2 2 nn0mulcli ⊢ ( 𝐶 · 𝐶 ) ∈ ℕ0
13 nn0ltp1le ⊢ ( ( ( ( 𝐴 · 𝐴 ) + ( 2 · 𝐴 ) ) ∈ ℕ0 ∧ ( 𝐶 · 𝐶 ) ∈ ℕ0 ) → ( ( ( 𝐴 · 𝐴 ) + ( 2 · 𝐴 ) ) < ( 𝐶 · 𝐶 ) ↔ ( ( ( 𝐴 · 𝐴 ) + ( 2 · 𝐴 ) ) + 1 ) ≤ ( 𝐶 · 𝐶 ) ) )
14 11 12 13 mp2an ⊢ ( ( ( 𝐴 · 𝐴 ) + ( 2 · 𝐴 ) ) < ( 𝐶 · 𝐶 ) ↔ ( ( ( 𝐴 · 𝐴 ) + ( 2 · 𝐴 ) ) + 1 ) ≤ ( 𝐶 · 𝐶 ) )
15 1 nn0cni ⊢ 𝐴 ∈ ℂ
16 ax-1cn ⊢ 1 ∈ ℂ
17 15 16 binom2i ⊢ ( ( 𝐴 + 1 ) ↑ 2 ) = ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 1 ) ) ) + ( 1 ↑ 2 ) )
18 15 16 addcli ⊢ ( 𝐴 + 1 ) ∈ ℂ
19 18 sqvali ⊢ ( ( 𝐴 + 1 ) ↑ 2 ) = ( ( 𝐴 + 1 ) · ( 𝐴 + 1 ) )
20 15 sqvali ⊢ ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 )
21 20 oveq1i ⊢ ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 1 ) ) ) = ( ( 𝐴 · 𝐴 ) + ( 2 · ( 𝐴 · 1 ) ) )
22 16 sqvali ⊢ ( 1 ↑ 2 ) = ( 1 · 1 )
23 21 22 oveq12i ⊢ ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 1 ) ) ) + ( 1 ↑ 2 ) ) = ( ( ( 𝐴 · 𝐴 ) + ( 2 · ( 𝐴 · 1 ) ) ) + ( 1 · 1 ) )
24 17 19 23 3eqtr3i ⊢ ( ( 𝐴 + 1 ) · ( 𝐴 + 1 ) ) = ( ( ( 𝐴 · 𝐴 ) + ( 2 · ( 𝐴 · 1 ) ) ) + ( 1 · 1 ) )
25 15 mulridi ⊢ ( 𝐴 · 1 ) = 𝐴
26 25 oveq2i ⊢ ( 2 · ( 𝐴 · 1 ) ) = ( 2 · 𝐴 )
27 26 oveq2i ⊢ ( ( 𝐴 · 𝐴 ) + ( 2 · ( 𝐴 · 1 ) ) ) = ( ( 𝐴 · 𝐴 ) + ( 2 · 𝐴 ) )
28 16 mulridi ⊢ ( 1 · 1 ) = 1
29 27 28 oveq12i ⊢ ( ( ( 𝐴 · 𝐴 ) + ( 2 · ( 𝐴 · 1 ) ) ) + ( 1 · 1 ) ) = ( ( ( 𝐴 · 𝐴 ) + ( 2 · 𝐴 ) ) + 1 )
30 24 29 eqtri ⊢ ( ( 𝐴 + 1 ) · ( 𝐴 + 1 ) ) = ( ( ( 𝐴 · 𝐴 ) + ( 2 · 𝐴 ) ) + 1 )
31 30 breq1i ⊢ ( ( ( 𝐴 + 1 ) · ( 𝐴 + 1 ) ) ≤ ( 𝐶 · 𝐶 ) ↔ ( ( ( 𝐴 · 𝐴 ) + ( 2 · 𝐴 ) ) + 1 ) ≤ ( 𝐶 · 𝐶 ) )
32 14 31 bitr4i ⊢ ( ( ( 𝐴 · 𝐴 ) + ( 2 · 𝐴 ) ) < ( 𝐶 · 𝐶 ) ↔ ( ( 𝐴 + 1 ) · ( 𝐴 + 1 ) ) ≤ ( 𝐶 · 𝐶 ) )
33 5 7 32 3bitr4i ⊢ ( 𝐴 < 𝐶 ↔ ( ( 𝐴 · 𝐴 ) + ( 2 · 𝐴 ) ) < ( 𝐶 · 𝐶 ) )