Metamath Proof Explorer

Theorem 01sqrexlem5

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

Ref Expression
Hypotheses 01sqrexlem1.1 ⊢ S = x ∈ ℝ + | x 2 ≤ A
01sqrexlem1.2 ⊢ B = sup S ℝ <
01sqrexlem5.3 ⊢ T = y | ∃ a ∈ S ∃ b ∈ S y = a ⁢ b
Assertion 01sqrexlem5 ⊢ A ∈ ℝ + ∧ A ≤ 1 → T ⊆ ℝ ∧ T ≠ ∅ ∧ ∃ v ∈ ℝ ∀ u ∈ T u ≤ v ∧ B 2 = sup T ℝ <

Proof

Step Hyp Ref Expression
1 01sqrexlem1.1 ⊢ S = x ∈ ℝ + | x 2 ≤ A
2 01sqrexlem1.2 ⊢ B = sup S ℝ <
3 01sqrexlem5.3 ⊢ T = y | ∃ a ∈ S ∃ b ∈ S y = a ⁢ b
4 1 ssrab3 ⊢ S ⊆ ℝ +
5 4 sseli ⊢ v ∈ S → v ∈ ℝ +
6 5 rpge0d ⊢ v ∈ S → 0 ≤ v
7 6 rgen ⊢ ∀ v ∈ S 0 ≤ v
8 1 2 01sqrexlem3 ⊢ A ∈ ℝ + ∧ A ≤ 1 → S ⊆ ℝ ∧ S ≠ ∅ ∧ ∃ v ∈ ℝ ∀ z ∈ S z ≤ v
9 pm4.24 ⊢ ∀ v ∈ S 0 ≤ v ↔ ∀ v ∈ S 0 ≤ v ∧ ∀ v ∈ S 0 ≤ v
10 9 3anbi1i ⊢ ∀ v ∈ S 0 ≤ v ∧ S ⊆ ℝ ∧ S ≠ ∅ ∧ ∃ v ∈ ℝ ∀ z ∈ S z ≤ v ∧ S ⊆ ℝ ∧ S ≠ ∅ ∧ ∃ v ∈ ℝ ∀ z ∈ S z ≤ v ↔ ∀ v ∈ S 0 ≤ v ∧ ∀ v ∈ S 0 ≤ v ∧ S ⊆ ℝ ∧ S ≠ ∅ ∧ ∃ v ∈ ℝ ∀ z ∈ S z ≤ v ∧ S ⊆ ℝ ∧ S ≠ ∅ ∧ ∃ v ∈ ℝ ∀ z ∈ S z ≤ v
11 3 10 supmullem2 ⊢ ∀ v ∈ S 0 ≤ v ∧ S ⊆ ℝ ∧ S ≠ ∅ ∧ ∃ v ∈ ℝ ∀ z ∈ S z ≤ v ∧ S ⊆ ℝ ∧ S ≠ ∅ ∧ ∃ v ∈ ℝ ∀ z ∈ S z ≤ v → T ⊆ ℝ ∧ T ≠ ∅ ∧ ∃ v ∈ ℝ ∀ u ∈ T u ≤ v
12 7 8 8 11 mp3an2i ⊢ A ∈ ℝ + ∧ A ≤ 1 → T ⊆ ℝ ∧ T ≠ ∅ ∧ ∃ v ∈ ℝ ∀ u ∈ T u ≤ v
13 1 2 01sqrexlem4 ⊢ A ∈ ℝ + ∧ A ≤ 1 → B ∈ ℝ + ∧ B ≤ 1
14 rpre ⊢ B ∈ ℝ + → B ∈ ℝ
15 14 adantr ⊢ B ∈ ℝ + ∧ B ≤ 1 → B ∈ ℝ
16 13 15 syl ⊢ A ∈ ℝ + ∧ A ≤ 1 → B ∈ ℝ
17 16 recnd ⊢ A ∈ ℝ + ∧ A ≤ 1 → B ∈ ℂ
18 17 sqvald ⊢ A ∈ ℝ + ∧ A ≤ 1 → B 2 = B ⁢ B
19 2 2 oveq12i ⊢ B ⁢ B = sup S ℝ < ⁢ sup S ℝ <
20 3 10 supmul ⊢ ∀ v ∈ S 0 ≤ v ∧ S ⊆ ℝ ∧ S ≠ ∅ ∧ ∃ v ∈ ℝ ∀ z ∈ S z ≤ v ∧ S ⊆ ℝ ∧ S ≠ ∅ ∧ ∃ v ∈ ℝ ∀ z ∈ S z ≤ v → sup S ℝ < ⁢ sup S ℝ < = sup T ℝ <
21 7 8 8 20 mp3an2i ⊢ A ∈ ℝ + ∧ A ≤ 1 → sup S ℝ < ⁢ sup S ℝ < = sup T ℝ <
22 19 21 eqtrid ⊢ A ∈ ℝ + ∧ A ≤ 1 → B ⁢ B = sup T ℝ <
23 18 22 eqtrd ⊢ A ∈ ℝ + ∧ A ≤ 1 → B 2 = sup T ℝ <
24 12 23 jca ⊢ A ∈ ℝ + ∧ A ≤ 1 → T ⊆ ℝ ∧ T ≠ ∅ ∧ ∃ v ∈ ℝ ∀ u ∈ T u ≤ v ∧ B 2 = sup T ℝ <