Metamath Proof Explorer


Theorem sqrlem4

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

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

Proof

Step Hyp Ref Expression
1 sqrlem1.1 𝑆 = { 𝑥 ∈ ℝ+ ∣ ( 𝑥 ↑ 2 ) ≤ 𝐴 }
2 sqrlem1.2 𝐵 = sup ( 𝑆 , ℝ , < )
3 1 2 sqrlem3 ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧𝑆 𝑧𝑦 ) )
4 suprcl ( ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧𝑆 𝑧𝑦 ) → sup ( 𝑆 , ℝ , < ) ∈ ℝ )
5 3 4 syl ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → sup ( 𝑆 , ℝ , < ) ∈ ℝ )
6 2 5 eqeltrid ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → 𝐵 ∈ ℝ )
7 rpgt0 ( 𝐴 ∈ ℝ+ → 0 < 𝐴 )
8 7 adantr ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → 0 < 𝐴 )
9 1 2 sqrlem2 ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → 𝐴𝑆 )
10 suprub ( ( ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧𝑆 𝑧𝑦 ) ∧ 𝐴𝑆 ) → 𝐴 ≤ sup ( 𝑆 , ℝ , < ) )
11 3 9 10 syl2anc ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → 𝐴 ≤ sup ( 𝑆 , ℝ , < ) )
12 11 2 breqtrrdi ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → 𝐴𝐵 )
13 0re 0 ∈ ℝ
14 rpre ( 𝐴 ∈ ℝ+𝐴 ∈ ℝ )
15 ltletr ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 0 < 𝐴𝐴𝐵 ) → 0 < 𝐵 ) )
16 13 14 6 15 mp3an2ani ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → ( ( 0 < 𝐴𝐴𝐵 ) → 0 < 𝐵 ) )
17 8 12 16 mp2and ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → 0 < 𝐵 )
18 6 17 elrpd ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → 𝐵 ∈ ℝ+ )
19 1 2 sqrlem1 ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → ∀ 𝑧𝑆 𝑧 ≤ 1 )
20 1re 1 ∈ ℝ
21 suprleub ( ( ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧𝑆 𝑧𝑦 ) ∧ 1 ∈ ℝ ) → ( sup ( 𝑆 , ℝ , < ) ≤ 1 ↔ ∀ 𝑧𝑆 𝑧 ≤ 1 ) )
22 3 20 21 sylancl ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → ( sup ( 𝑆 , ℝ , < ) ≤ 1 ↔ ∀ 𝑧𝑆 𝑧 ≤ 1 ) )
23 19 22 mpbird ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → sup ( 𝑆 , ℝ , < ) ≤ 1 )
24 2 23 eqbrtrid ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → 𝐵 ≤ 1 )
25 18 24 jca ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → ( 𝐵 ∈ ℝ+𝐵 ≤ 1 ) )