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

Metamath Proof Explorer

Theorem 01sqrexlem4

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

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

Proof

Step Hyp Ref Expression
1 01sqrexlem1.1 ⊢ 𝑆 = { 𝑥 ∈ ℝ+ ∣ ( 𝑥 ↑ 2 ) ≤ 𝐴 }
2 01sqrexlem1.2 ⊢ 𝐵 = sup ( 𝑆 , ℝ , < )
3 1 2 01sqrexlem3 ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 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 01sqrexlem2 ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 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 01sqrexlem1 ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 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 ) )