Metamath Proof Explorer

Theorem sqrlem5

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

Ref Expression
Hypotheses sqrlem1.1 ⊢ 𝑆 = { 𝑥 ∈ ℝ+ ∣ ( 𝑥 ↑ 2 ) ≤ 𝐴 }
sqrlem1.2 ⊢ 𝐵 = sup ( 𝑆 , ℝ , < )
sqrlem5.3 ⊢ 𝑇 = { 𝑦 ∣ ∃ 𝑎 ∈ 𝑆 ∃ 𝑏 ∈ 𝑆 𝑦 = ( 𝑎 · 𝑏 ) }
Assertion sqrlem5 ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( ( 𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃ 𝑣 ∈ ℝ ∀ 𝑢 ∈ 𝑇 𝑢 ≤ 𝑣 ) ∧ ( 𝐵 ↑ 2 ) = sup ( 𝑇 , ℝ , < ) ) )

Proof

Step Hyp Ref Expression
1 sqrlem1.1 ⊢ 𝑆 = { 𝑥 ∈ ℝ+ ∣ ( 𝑥 ↑ 2 ) ≤ 𝐴 }
2 sqrlem1.2 ⊢ 𝐵 = sup ( 𝑆 , ℝ , < )
3 sqrlem5.3 ⊢ 𝑇 = { 𝑦 ∣ ∃ 𝑎 ∈ 𝑆 ∃ 𝑏 ∈ 𝑆 𝑦 = ( 𝑎 · 𝑏 ) }
4 1 ssrab3 ⊢ 𝑆 ⊆ ℝ+
5 4 sseli ⊢ ( 𝑣 ∈ 𝑆 → 𝑣 ∈ ℝ+ )
6 5 rpge0d ⊢ ( 𝑣 ∈ 𝑆 → 0 ≤ 𝑣 )
7 6 rgen ⊢ ∀ 𝑣 ∈ 𝑆 0 ≤ 𝑣
8 1 2 sqrlem3 ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑣 ∈ ℝ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝑣 ) )
9 pm4.24 ⊢ ( ∀ 𝑣 ∈ 𝑆 0 ≤ 𝑣 ↔ ( ∀ 𝑣 ∈ 𝑆 0 ≤ 𝑣 ∧ ∀ 𝑣 ∈ 𝑆 0 ≤ 𝑣 ) )
10 9 3anbi1i ⊢ ( ( ∀ 𝑣 ∈ 𝑆 0 ≤ 𝑣 ∧ ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑣 ∈ ℝ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝑣 ) ∧ ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑣 ∈ ℝ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝑣 ) ) ↔ ( ( ∀ 𝑣 ∈ 𝑆 0 ≤ 𝑣 ∧ ∀ 𝑣 ∈ 𝑆 0 ≤ 𝑣 ) ∧ ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑣 ∈ ℝ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝑣 ) ∧ ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑣 ∈ ℝ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝑣 ) ) )
11 3 10 supmullem2 ⊢ ( ( ∀ 𝑣 ∈ 𝑆 0 ≤ 𝑣 ∧ ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑣 ∈ ℝ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝑣 ) ∧ ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑣 ∈ ℝ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝑣 ) ) → ( 𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃ 𝑣 ∈ ℝ ∀ 𝑢 ∈ 𝑇 𝑢 ≤ 𝑣 ) )
12 7 8 8 11 mp3an2i ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( 𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃ 𝑣 ∈ ℝ ∀ 𝑢 ∈ 𝑇 𝑢 ≤ 𝑣 ) )
13 1 2 sqrlem4 ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≤ 1 ) )
14 rpre ⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ∈ ℝ )
15 14 adantr ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≤ 1 ) → 𝐵 ∈ ℝ )
16 13 15 syl ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → 𝐵 ∈ ℝ )
17 16 recnd ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → 𝐵 ∈ ℂ )
18 17 sqvald ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( 𝐵 ↑ 2 ) = ( 𝐵 · 𝐵 ) )
19 2 2 oveq12i ⊢ ( 𝐵 · 𝐵 ) = ( sup ( 𝑆 , ℝ , < ) · sup ( 𝑆 , ℝ , < ) )
20 3 10 supmul ⊢ ( ( ∀ 𝑣 ∈ 𝑆 0 ≤ 𝑣 ∧ ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑣 ∈ ℝ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝑣 ) ∧ ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑣 ∈ ℝ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝑣 ) ) → ( sup ( 𝑆 , ℝ , < ) · sup ( 𝑆 , ℝ , < ) ) = sup ( 𝑇 , ℝ , < ) )
21 7 8 8 20 mp3an2i ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( sup ( 𝑆 , ℝ , < ) · sup ( 𝑆 , ℝ , < ) ) = sup ( 𝑇 , ℝ , < ) )
22 19 21 syl5eq ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( 𝐵 · 𝐵 ) = sup ( 𝑇 , ℝ , < ) )
23 18 22 eqtrd ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( 𝐵 ↑ 2 ) = sup ( 𝑇 , ℝ , < ) )
24 12 23 jca ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( ( 𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃ 𝑣 ∈ ℝ ∀ 𝑢 ∈ 𝑇 𝑢 ≤ 𝑣 ) ∧ ( 𝐵 ↑ 2 ) = sup ( 𝑇 , ℝ , < ) ) )