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 ) )