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

Metamath Proof Explorer

Theorem lt2msq1

Description: Lemma for lt2msq . (Contributed by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion lt2msq1 ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝐴 · 𝐴 ) < ( 𝐵 · 𝐵 ) )

Proof

Step Hyp Ref Expression
1 simp1l ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐴 ∈ ℝ )
2 1 1 remulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝐴 · 𝐴 ) ∈ ℝ )
3 simp2 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐵 ∈ ℝ )
4 3 1 remulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝐵 · 𝐴 ) ∈ ℝ )
5 3 3 remulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝐵 · 𝐵 ) ∈ ℝ )
6 simp1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) )
7 simp3 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐴 < 𝐵 )
8 1 3 7 ltled ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐴 ≤ 𝐵 )
9 lemul1a ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 · 𝐴 ) ≤ ( 𝐵 · 𝐴 ) )
10 1 3 6 8 9 syl31anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝐴 · 𝐴 ) ≤ ( 𝐵 · 𝐴 ) )
11 0red ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 0 ∈ ℝ )
12 simp1r ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 0 ≤ 𝐴 )
13 11 1 3 12 7 lelttrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 0 < 𝐵 )
14 ltmul2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( 𝐴 < 𝐵 ↔ ( 𝐵 · 𝐴 ) < ( 𝐵 · 𝐵 ) ) )
15 1 3 3 13 14 syl112anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝐴 < 𝐵 ↔ ( 𝐵 · 𝐴 ) < ( 𝐵 · 𝐵 ) ) )
16 7 15 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝐵 · 𝐴 ) < ( 𝐵 · 𝐵 ) )
17 2 4 5 10 16 lelttrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝐴 · 𝐴 ) < ( 𝐵 · 𝐵 ) )