Metamath Proof Explorer


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 )