Theorem sqrlem6

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

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

Proof

Step	Hyp	Ref	Expression
1		sqrlem1.1	⊢ 𝑆 = { 𝑥 ∈ ℝ+ ∣ ( 𝑥 ↑ 2 ) ≤ 𝐴 }
2		sqrlem1.2	⊢ 𝐵 = sup ( 𝑆 , ℝ , < )
3		sqrlem5.3	⊢ 𝑇 = { 𝑦 ∣ ∃ 𝑎 ∈ 𝑆 ∃ 𝑏 ∈ 𝑆 𝑦 = ( 𝑎 · 𝑏 ) }
4	1 2 3	sqrlem5	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 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	sqrlem3	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 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	syl5bi	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 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 ) ≤ 𝐴 )