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	mulid1i	⊢ ( 𝐴 · 1 ) = 𝐴
26	25	oveq2i	⊢ ( 2 · ( 𝐴 · 1 ) ) = ( 2 · 𝐴 )
27	26	oveq2i	⊢ ( ( 𝐴 · 𝐴 ) + ( 2 · ( 𝐴 · 1 ) ) ) = ( ( 𝐴 · 𝐴 ) + ( 2 · 𝐴 ) )
28	16	mulid1i	⊢ ( 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 · 𝐴 ) ) < ( 𝐶 · 𝐶 ) )