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

Metamath Proof Explorer

Theorem 01sqrexlem6

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

Ref Expression
Hypotheses 01sqrexlem1.1 ⊢ 𝑆 = { 𝑥 ∈ ℝ+ ∣ ( 𝑥 ↑ 2 ) ≤ 𝐴 }
01sqrexlem1.2 ⊢ 𝐵 = sup ( 𝑆 , ℝ , < )
01sqrexlem5.3 ⊢ 𝑇 = { 𝑦 ∣ ∃ 𝑎 ∈ 𝑆 ∃ 𝑏 ∈ 𝑆 𝑦 = ( 𝑎 · 𝑏 ) }
Assertion 01sqrexlem6 ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( 𝐵 ↑ 2 ) ≤ 𝐴 )

Proof

Step Hyp Ref Expression
1 01sqrexlem1.1 ⊢ 𝑆 = { 𝑥 ∈ ℝ+ ∣ ( 𝑥 ↑ 2 ) ≤ 𝐴 }
2 01sqrexlem1.2 ⊢ 𝐵 = sup ( 𝑆 , ℝ , < )
3 01sqrexlem5.3 ⊢ 𝑇 = { 𝑦 ∣ ∃ 𝑎 ∈ 𝑆 ∃ 𝑏 ∈ 𝑆 𝑦 = ( 𝑎 · 𝑏 ) }
4 1 2 3 01sqrexlem5 ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( ( 𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃ 𝑣 ∈ ℝ ∀ 𝑢 ∈ 𝑇 𝑢 ≤ 𝑣 ) ∧ ( 𝐵 ↑ 2 ) = sup ( 𝑇 , ℝ , < ) ) )
5 4 simprd ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( 𝐵 ↑ 2 ) = sup ( 𝑇 , ℝ , < ) )
6 vex ⊢ 𝑣 ∈ V
7 eqeq1 ⊢ ( 𝑦 = 𝑣 → ( 𝑦 = ( 𝑎 · 𝑏 ) ↔ 𝑣 = ( 𝑎 · 𝑏 ) ) )
8 7 2rexbidv ⊢ ( 𝑦 = 𝑣 → ( ∃ 𝑎 ∈ 𝑆 ∃ 𝑏 ∈ 𝑆 𝑦 = ( 𝑎 · 𝑏 ) ↔ ∃ 𝑎 ∈ 𝑆 ∃ 𝑏 ∈ 𝑆 𝑣 = ( 𝑎 · 𝑏 ) ) )
9 6 8 3 elab2 ⊢ ( 𝑣 ∈ 𝑇 ↔ ∃ 𝑎 ∈ 𝑆 ∃ 𝑏 ∈ 𝑆 𝑣 = ( 𝑎 · 𝑏 ) )
10 oveq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 ↑ 2 ) = ( 𝑎 ↑ 2 ) )
11 10 breq1d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑥 ↑ 2 ) ≤ 𝐴 ↔ ( 𝑎 ↑ 2 ) ≤ 𝐴 ) )
12 11 1 elrab2 ⊢ ( 𝑎 ∈ 𝑆 ↔ ( 𝑎 ∈ ℝ+ ∧ ( 𝑎 ↑ 2 ) ≤ 𝐴 ) )
13 12 simplbi ⊢ ( 𝑎 ∈ 𝑆 → 𝑎 ∈ ℝ+ )
14 oveq1 ⊢ ( 𝑥 = 𝑏 → ( 𝑥 ↑ 2 ) = ( 𝑏 ↑ 2 ) )
15 14 breq1d ⊢ ( 𝑥 = 𝑏 → ( ( 𝑥 ↑ 2 ) ≤ 𝐴 ↔ ( 𝑏 ↑ 2 ) ≤ 𝐴 ) )
16 15 1 elrab2 ⊢ ( 𝑏 ∈ 𝑆 ↔ ( 𝑏 ∈ ℝ+ ∧ ( 𝑏 ↑ 2 ) ≤ 𝐴 ) )
17 16 simplbi ⊢ ( 𝑏 ∈ 𝑆 → 𝑏 ∈ ℝ+ )
18 rpre ⊢ ( 𝑎 ∈ ℝ+ → 𝑎 ∈ ℝ )
19 18 adantr ⊢ ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) → 𝑎 ∈ ℝ )
20 rpre ⊢ ( 𝑏 ∈ ℝ+ → 𝑏 ∈ ℝ )
21 20 adantl ⊢ ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) → 𝑏 ∈ ℝ )
22 rpgt0 ⊢ ( 𝑏 ∈ ℝ+ → 0 < 𝑏 )
23 22 adantl ⊢ ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) → 0 < 𝑏 )
24 lemul1 ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ ( 𝑏 ∈ ℝ ∧ 0 < 𝑏 ) ) → ( 𝑎 ≤ 𝑏 ↔ ( 𝑎 · 𝑏 ) ≤ ( 𝑏 · 𝑏 ) ) )
25 19 21 21 23 24 syl112anc ⊢ ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) → ( 𝑎 ≤ 𝑏 ↔ ( 𝑎 · 𝑏 ) ≤ ( 𝑏 · 𝑏 ) ) )
26 13 17 25 syl2an ⊢ ( ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) → ( 𝑎 ≤ 𝑏 ↔ ( 𝑎 · 𝑏 ) ≤ ( 𝑏 · 𝑏 ) ) )
27 17 rpcnd ⊢ ( 𝑏 ∈ 𝑆 → 𝑏 ∈ ℂ )
28 27 sqvald ⊢ ( 𝑏 ∈ 𝑆 → ( 𝑏 ↑ 2 ) = ( 𝑏 · 𝑏 ) )
29 28 breq2d ⊢ ( 𝑏 ∈ 𝑆 → ( ( 𝑎 · 𝑏 ) ≤ ( 𝑏 ↑ 2 ) ↔ ( 𝑎 · 𝑏 ) ≤ ( 𝑏 · 𝑏 ) ) )
30 29 adantl ⊢ ( ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) → ( ( 𝑎 · 𝑏 ) ≤ ( 𝑏 ↑ 2 ) ↔ ( 𝑎 · 𝑏 ) ≤ ( 𝑏 · 𝑏 ) ) )
31 26 30 bitr4d ⊢ ( ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) → ( 𝑎 ≤ 𝑏 ↔ ( 𝑎 · 𝑏 ) ≤ ( 𝑏 ↑ 2 ) ) )
32 31 adantl ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → ( 𝑎 ≤ 𝑏 ↔ ( 𝑎 · 𝑏 ) ≤ ( 𝑏 ↑ 2 ) ) )
33 16 simprbi ⊢ ( 𝑏 ∈ 𝑆 → ( 𝑏 ↑ 2 ) ≤ 𝐴 )
34 33 ad2antll ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → ( 𝑏 ↑ 2 ) ≤ 𝐴 )
35 13 rpred ⊢ ( 𝑎 ∈ 𝑆 → 𝑎 ∈ ℝ )
36 17 rpred ⊢ ( 𝑏 ∈ 𝑆 → 𝑏 ∈ ℝ )
37 remulcl ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( 𝑎 · 𝑏 ) ∈ ℝ )
38 35 36 37 syl2an ⊢ ( ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) → ( 𝑎 · 𝑏 ) ∈ ℝ )
39 38 adantl ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → ( 𝑎 · 𝑏 ) ∈ ℝ )
40 36 resqcld ⊢ ( 𝑏 ∈ 𝑆 → ( 𝑏 ↑ 2 ) ∈ ℝ )
41 40 ad2antll ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → ( 𝑏 ↑ 2 ) ∈ ℝ )
42 rpre ⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ )
43 42 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → 𝐴 ∈ ℝ )
44 letr ⊢ ( ( ( 𝑎 · 𝑏 ) ∈ ℝ ∧ ( 𝑏 ↑ 2 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( ( 𝑎 · 𝑏 ) ≤ ( 𝑏 ↑ 2 ) ∧ ( 𝑏 ↑ 2 ) ≤ 𝐴 ) → ( 𝑎 · 𝑏 ) ≤ 𝐴 ) )
45 39 41 43 44 syl3anc ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → ( ( ( 𝑎 · 𝑏 ) ≤ ( 𝑏 ↑ 2 ) ∧ ( 𝑏 ↑ 2 ) ≤ 𝐴 ) → ( 𝑎 · 𝑏 ) ≤ 𝐴 ) )
46 34 45 mpan2d ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → ( ( 𝑎 · 𝑏 ) ≤ ( 𝑏 ↑ 2 ) → ( 𝑎 · 𝑏 ) ≤ 𝐴 ) )
47 32 46 sylbid ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → ( 𝑎 ≤ 𝑏 → ( 𝑎 · 𝑏 ) ≤ 𝐴 ) )
48 rpgt0 ⊢ ( 𝑎 ∈ ℝ+ → 0 < 𝑎 )
49 48 adantr ⊢ ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) → 0 < 𝑎 )
50 lemul2 ⊢ ( ( 𝑏 ∈ ℝ ∧ 𝑎 ∈ ℝ ∧ ( 𝑎 ∈ ℝ ∧ 0 < 𝑎 ) ) → ( 𝑏 ≤ 𝑎 ↔ ( 𝑎 · 𝑏 ) ≤ ( 𝑎 · 𝑎 ) ) )
51 21 19 19 49 50 syl112anc ⊢ ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) → ( 𝑏 ≤ 𝑎 ↔ ( 𝑎 · 𝑏 ) ≤ ( 𝑎 · 𝑎 ) ) )
52 13 17 51 syl2an ⊢ ( ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) → ( 𝑏 ≤ 𝑎 ↔ ( 𝑎 · 𝑏 ) ≤ ( 𝑎 · 𝑎 ) ) )
53 13 rpcnd ⊢ ( 𝑎 ∈ 𝑆 → 𝑎 ∈ ℂ )
54 53 sqvald ⊢ ( 𝑎 ∈ 𝑆 → ( 𝑎 ↑ 2 ) = ( 𝑎 · 𝑎 ) )
55 54 breq2d ⊢ ( 𝑎 ∈ 𝑆 → ( ( 𝑎 · 𝑏 ) ≤ ( 𝑎 ↑ 2 ) ↔ ( 𝑎 · 𝑏 ) ≤ ( 𝑎 · 𝑎 ) ) )
56 55 adantr ⊢ ( ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) → ( ( 𝑎 · 𝑏 ) ≤ ( 𝑎 ↑ 2 ) ↔ ( 𝑎 · 𝑏 ) ≤ ( 𝑎 · 𝑎 ) ) )
57 52 56 bitr4d ⊢ ( ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) → ( 𝑏 ≤ 𝑎 ↔ ( 𝑎 · 𝑏 ) ≤ ( 𝑎 ↑ 2 ) ) )
58 57 adantl ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → ( 𝑏 ≤ 𝑎 ↔ ( 𝑎 · 𝑏 ) ≤ ( 𝑎 ↑ 2 ) ) )
59 12 simprbi ⊢ ( 𝑎 ∈ 𝑆 → ( 𝑎 ↑ 2 ) ≤ 𝐴 )
60 59 ad2antrl ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → ( 𝑎 ↑ 2 ) ≤ 𝐴 )
61 35 resqcld ⊢ ( 𝑎 ∈ 𝑆 → ( 𝑎 ↑ 2 ) ∈ ℝ )
62 61 ad2antrl ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → ( 𝑎 ↑ 2 ) ∈ ℝ )
63 letr ⊢ ( ( ( 𝑎 · 𝑏 ) ∈ ℝ ∧ ( 𝑎 ↑ 2 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( ( 𝑎 · 𝑏 ) ≤ ( 𝑎 ↑ 2 ) ∧ ( 𝑎 ↑ 2 ) ≤ 𝐴 ) → ( 𝑎 · 𝑏 ) ≤ 𝐴 ) )
64 39 62 43 63 syl3anc ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → ( ( ( 𝑎 · 𝑏 ) ≤ ( 𝑎 ↑ 2 ) ∧ ( 𝑎 ↑ 2 ) ≤ 𝐴 ) → ( 𝑎 · 𝑏 ) ≤ 𝐴 ) )
65 60 64 mpan2d ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → ( ( 𝑎 · 𝑏 ) ≤ ( 𝑎 ↑ 2 ) → ( 𝑎 · 𝑏 ) ≤ 𝐴 ) )
66 58 65 sylbid ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → ( 𝑏 ≤ 𝑎 → ( 𝑎 · 𝑏 ) ≤ 𝐴 ) )
67 1 2 01sqrexlem3 ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑣 ∈ 𝑆 𝑣 ≤ 𝑦 ) )
68 67 simp1d ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → 𝑆 ⊆ ℝ )
69 68 sseld ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( 𝑎 ∈ 𝑆 → 𝑎 ∈ ℝ ) )
70 68 sseld ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( 𝑏 ∈ 𝑆 → 𝑏 ∈ ℝ ) )
71 69 70 anim12d ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) → ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) )
72 71 imp ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) )
73 letric ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( 𝑎 ≤ 𝑏 ∨ 𝑏 ≤ 𝑎 ) )
74 72 73 syl ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → ( 𝑎 ≤ 𝑏 ∨ 𝑏 ≤ 𝑎 ) )
75 47 66 74 mpjaod ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → ( 𝑎 · 𝑏 ) ≤ 𝐴 )
76 75 ex ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) → ( 𝑎 · 𝑏 ) ≤ 𝐴 ) )
77 breq1 ⊢ ( 𝑣 = ( 𝑎 · 𝑏 ) → ( 𝑣 ≤ 𝐴 ↔ ( 𝑎 · 𝑏 ) ≤ 𝐴 ) )
78 77 biimprcd ⊢ ( ( 𝑎 · 𝑏 ) ≤ 𝐴 → ( 𝑣 = ( 𝑎 · 𝑏 ) → 𝑣 ≤ 𝐴 ) )
79 76 78 syl6 ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) → ( 𝑣 = ( 𝑎 · 𝑏 ) → 𝑣 ≤ 𝐴 ) ) )
80 79 rexlimdvv ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( ∃ 𝑎 ∈ 𝑆 ∃ 𝑏 ∈ 𝑆 𝑣 = ( 𝑎 · 𝑏 ) → 𝑣 ≤ 𝐴 ) )
81 9 80 biimtrid ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( 𝑣 ∈ 𝑇 → 𝑣 ≤ 𝐴 ) )
82 81 ralrimiv ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ∀ 𝑣 ∈ 𝑇 𝑣 ≤ 𝐴 )
83 4 simpld ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( 𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃ 𝑣 ∈ ℝ ∀ 𝑢 ∈ 𝑇 𝑢 ≤ 𝑣 ) )
84 42 adantr ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → 𝐴 ∈ ℝ )
85 suprleub ⊢ ( ( ( 𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃ 𝑣 ∈ ℝ ∀ 𝑢 ∈ 𝑇 𝑢 ≤ 𝑣 ) ∧ 𝐴 ∈ ℝ ) → ( sup ( 𝑇 , ℝ , < ) ≤ 𝐴 ↔ ∀ 𝑣 ∈ 𝑇 𝑣 ≤ 𝐴 ) )
86 83 84 85 syl2anc ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( sup ( 𝑇 , ℝ , < ) ≤ 𝐴 ↔ ∀ 𝑣 ∈ 𝑇 𝑣 ≤ 𝐴 ) )
87 82 86 mpbird ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → sup ( 𝑇 , ℝ , < ) ≤ 𝐴 )
88 5 87 eqbrtrd ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( 𝐵 ↑ 2 ) ≤ 𝐴 )