Theorem sqrlem1

Description: Lemma for 01sqrex . (Contributed by Mario Carneiro, 10-Jul-2013)

	Ref	Expression
Hypotheses	sqrlem1.1	⊢ 𝑆 = { 𝑥 ∈ ℝ+ ∣ ( 𝑥 ↑ 2 ) ≤ 𝐴 }
	sqrlem1.2	⊢ 𝐵 = sup ( 𝑆 , ℝ , < )
Assertion	sqrlem1	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 1 )

Proof

Step	Hyp	Ref	Expression
1		sqrlem1.1	⊢ 𝑆 = { 𝑥 ∈ ℝ+ ∣ ( 𝑥 ↑ 2 ) ≤ 𝐴 }
2		sqrlem1.2	⊢ 𝐵 = sup ( 𝑆 , ℝ , < )
3		oveq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ↑ 2 ) = ( 𝑦 ↑ 2 ) )
4	3	breq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ↑ 2 ) ≤ 𝐴 ↔ ( 𝑦 ↑ 2 ) ≤ 𝐴 ) )
5	4 1	elrab2	⊢ ( 𝑦 ∈ 𝑆 ↔ ( 𝑦 ∈ ℝ+ ∧ ( 𝑦 ↑ 2 ) ≤ 𝐴 ) )
6		simprr	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) ∧ ( 𝑦 ∈ ℝ+ ∧ ( 𝑦 ↑ 2 ) ≤ 𝐴 ) ) → ( 𝑦 ↑ 2 ) ≤ 𝐴 )
7		simplr	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) ∧ ( 𝑦 ∈ ℝ+ ∧ ( 𝑦 ↑ 2 ) ≤ 𝐴 ) ) → 𝐴 ≤ 1 )
8		rpre	⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ )
9	8	ad2antrl	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) ∧ ( 𝑦 ∈ ℝ+ ∧ ( 𝑦 ↑ 2 ) ≤ 𝐴 ) ) → 𝑦 ∈ ℝ )
10	9	resqcld	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) ∧ ( 𝑦 ∈ ℝ+ ∧ ( 𝑦 ↑ 2 ) ≤ 𝐴 ) ) → ( 𝑦 ↑ 2 ) ∈ ℝ )
11		rpre	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ )
12	11	ad2antrr	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) ∧ ( 𝑦 ∈ ℝ+ ∧ ( 𝑦 ↑ 2 ) ≤ 𝐴 ) ) → 𝐴 ∈ ℝ )
13		1re	⊢ 1 ∈ ℝ
14		letr	⊢ ( ( ( 𝑦 ↑ 2 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( ( 𝑦 ↑ 2 ) ≤ 𝐴 ∧ 𝐴 ≤ 1 ) → ( 𝑦 ↑ 2 ) ≤ 1 ) )
15	13 14	mp3an3	⊢ ( ( ( 𝑦 ↑ 2 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( ( 𝑦 ↑ 2 ) ≤ 𝐴 ∧ 𝐴 ≤ 1 ) → ( 𝑦 ↑ 2 ) ≤ 1 ) )
16	10 12 15	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) ∧ ( 𝑦 ∈ ℝ+ ∧ ( 𝑦 ↑ 2 ) ≤ 𝐴 ) ) → ( ( ( 𝑦 ↑ 2 ) ≤ 𝐴 ∧ 𝐴 ≤ 1 ) → ( 𝑦 ↑ 2 ) ≤ 1 ) )
17	6 7 16	mp2and	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) ∧ ( 𝑦 ∈ ℝ+ ∧ ( 𝑦 ↑ 2 ) ≤ 𝐴 ) ) → ( 𝑦 ↑ 2 ) ≤ 1 )
18		sq1	⊢ ( 1 ↑ 2 ) = 1
19	17 18	breqtrrdi	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) ∧ ( 𝑦 ∈ ℝ+ ∧ ( 𝑦 ↑ 2 ) ≤ 𝐴 ) ) → ( 𝑦 ↑ 2 ) ≤ ( 1 ↑ 2 ) )
20		rpge0	⊢ ( 𝑦 ∈ ℝ+ → 0 ≤ 𝑦 )
21	20	ad2antrl	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) ∧ ( 𝑦 ∈ ℝ+ ∧ ( 𝑦 ↑ 2 ) ≤ 𝐴 ) ) → 0 ≤ 𝑦 )
22		0le1	⊢ 0 ≤ 1
23		le2sq	⊢ ( ( ( 𝑦 ∈ ℝ ∧ 0 ≤ 𝑦 ) ∧ ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ) → ( 𝑦 ≤ 1 ↔ ( 𝑦 ↑ 2 ) ≤ ( 1 ↑ 2 ) ) )
24	13 22 23	mpanr12	⊢ ( ( 𝑦 ∈ ℝ ∧ 0 ≤ 𝑦 ) → ( 𝑦 ≤ 1 ↔ ( 𝑦 ↑ 2 ) ≤ ( 1 ↑ 2 ) ) )
25	9 21 24	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) ∧ ( 𝑦 ∈ ℝ+ ∧ ( 𝑦 ↑ 2 ) ≤ 𝐴 ) ) → ( 𝑦 ≤ 1 ↔ ( 𝑦 ↑ 2 ) ≤ ( 1 ↑ 2 ) ) )
26	19 25	mpbird	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) ∧ ( 𝑦 ∈ ℝ+ ∧ ( 𝑦 ↑ 2 ) ≤ 𝐴 ) ) → 𝑦 ≤ 1 )
27	26	ex	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( ( 𝑦 ∈ ℝ+ ∧ ( 𝑦 ↑ 2 ) ≤ 𝐴 ) → 𝑦 ≤ 1 ) )
28	5 27	syl5bi	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( 𝑦 ∈ 𝑆 → 𝑦 ≤ 1 ) )
29	28	ralrimiv	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 1 )