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 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝐴 · 𝐴 ) < ( 𝐵 · 𝐵 ) )