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	eqtrid	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( 𝐵 · 𝐵 ) = sup ( 𝑇 , ℝ , < ) )
23	18 22	eqtrd	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( 𝐵 ↑ 2 ) = sup ( 𝑇 , ℝ , < ) )
24	12 23	jca	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( ( 𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃ 𝑣 ∈ ℝ ∀ 𝑢 ∈ 𝑇 𝑢 ≤ 𝑣 ) ∧ ( 𝐵 ↑ 2 ) = sup ( 𝑇 , ℝ , < ) ) )