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

Metamath Proof Explorer

Theorem nn0opthlem2

Description: Lemma for nn0opthi . (Contributed by Raph Levien, 10-Dec-2002) (Revised by Scott Fenton, 8-Sep-2010)

Ref Expression
Hypotheses nn0opth.1 ⊢ 𝐴 ∈ ℕ0
nn0opth.2 ⊢ 𝐵 ∈ ℕ0
nn0opth.3 ⊢ 𝐶 ∈ ℕ0
nn0opth.4 ⊢ 𝐷 ∈ ℕ0
Assertion nn0opthlem2 ( ( 𝐴 + 𝐵 ) < 𝐶 → ( ( 𝐶 · 𝐶 ) + 𝐷 ) ≠ ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) )

Proof

Step Hyp Ref Expression
1 nn0opth.1 ⊢ 𝐴 ∈ ℕ0
2 nn0opth.2 ⊢ 𝐵 ∈ ℕ0
3 nn0opth.3 ⊢ 𝐶 ∈ ℕ0
4 nn0opth.4 ⊢ 𝐷 ∈ ℕ0
5 1 2 nn0addcli ⊢ ( 𝐴 + 𝐵 ) ∈ ℕ0
6 5 3 nn0opthlem1 ⊢ ( ( 𝐴 + 𝐵 ) < 𝐶 ↔ ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + ( 2 · ( 𝐴 + 𝐵 ) ) ) < ( 𝐶 · 𝐶 ) )
7 2 nn0rei ⊢ 𝐵 ∈ ℝ
8 7 1 nn0addge2i ⊢ 𝐵 ≤ ( 𝐴 + 𝐵 )
9 5 2 nn0lele2xi ⊢ ( 𝐵 ≤ ( 𝐴 + 𝐵 ) → 𝐵 ≤ ( 2 · ( 𝐴 + 𝐵 ) ) )
10 2re ⊢ 2 ∈ ℝ
11 5 nn0rei ⊢ ( 𝐴 + 𝐵 ) ∈ ℝ
12 10 11 remulcli ⊢ ( 2 · ( 𝐴 + 𝐵 ) ) ∈ ℝ
13 11 11 remulcli ⊢ ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) ∈ ℝ
14 7 12 13 leadd2i ⊢ ( 𝐵 ≤ ( 2 · ( 𝐴 + 𝐵 ) ) ↔ ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) ≤ ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + ( 2 · ( 𝐴 + 𝐵 ) ) ) )
15 9 14 sylib ⊢ ( 𝐵 ≤ ( 𝐴 + 𝐵 ) → ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) ≤ ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + ( 2 · ( 𝐴 + 𝐵 ) ) ) )
16 8 15 ax-mp ⊢ ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) ≤ ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + ( 2 · ( 𝐴 + 𝐵 ) ) )
17 13 7 readdcli ⊢ ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) ∈ ℝ
18 13 12 readdcli ⊢ ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + ( 2 · ( 𝐴 + 𝐵 ) ) ) ∈ ℝ
19 3 nn0rei ⊢ 𝐶 ∈ ℝ
20 19 19 remulcli ⊢ ( 𝐶 · 𝐶 ) ∈ ℝ
21 17 18 20 lelttri ⊢ ( ( ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) ≤ ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + ( 2 · ( 𝐴 + 𝐵 ) ) ) ∧ ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + ( 2 · ( 𝐴 + 𝐵 ) ) ) < ( 𝐶 · 𝐶 ) ) → ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) < ( 𝐶 · 𝐶 ) )
22 16 21 mpan ⊢ ( ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + ( 2 · ( 𝐴 + 𝐵 ) ) ) < ( 𝐶 · 𝐶 ) → ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) < ( 𝐶 · 𝐶 ) )
23 6 22 sylbi ⊢ ( ( 𝐴 + 𝐵 ) < 𝐶 → ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) < ( 𝐶 · 𝐶 ) )
24 20 4 nn0addge1i ⊢ ( 𝐶 · 𝐶 ) ≤ ( ( 𝐶 · 𝐶 ) + 𝐷 )
25 4 nn0rei ⊢ 𝐷 ∈ ℝ
26 20 25 readdcli ⊢ ( ( 𝐶 · 𝐶 ) + 𝐷 ) ∈ ℝ
27 17 20 26 ltletri ⊢ ( ( ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) < ( 𝐶 · 𝐶 ) ∧ ( 𝐶 · 𝐶 ) ≤ ( ( 𝐶 · 𝐶 ) + 𝐷 ) ) → ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) < ( ( 𝐶 · 𝐶 ) + 𝐷 ) )
28 24 27 mpan2 ⊢ ( ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) < ( 𝐶 · 𝐶 ) → ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) < ( ( 𝐶 · 𝐶 ) + 𝐷 ) )
29 17 26 ltnei ⊢ ( ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) < ( ( 𝐶 · 𝐶 ) + 𝐷 ) → ( ( 𝐶 · 𝐶 ) + 𝐷 ) ≠ ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) )
30 23 28 29 3syl ⊢ ( ( 𝐴 + 𝐵 ) < 𝐶 → ( ( 𝐶 · 𝐶 ) + 𝐷 ) ≠ ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) )