aalioulem3

	Ref	Expression
Hypotheses	aalioulem2.a	$⊢ N = \deg (F)$
	aalioulem2.b	$⊢ φ \to F \in Poly (ℤ)$
	aalioulem2.c	$⊢ φ \to N \in ℕ$
	aalioulem2.d	$⊢ φ \to A \in ℝ$
	aalioulem3.e	$⊢ φ \to F (A) = 0$
Assertion	aalioulem3	$⊢ φ \to \exists x \in ℝ^{+} \forall r \in ℝ (\|A - r\| \leq 1 \to x \|F (r)\| \leq \|A - r\|)$

Proof

Step	Hyp	Ref	Expression
1		aalioulem2.a	$⊢ N = \deg (F)$
2		aalioulem2.b	$⊢ φ \to F \in Poly (ℤ)$
3		aalioulem2.c	$⊢ φ \to N \in ℕ$
4		aalioulem2.d	$⊢ φ \to A \in ℝ$
5		aalioulem3.e	$⊢ φ \to F (A) = 0$
6		1re	$⊢ 1 \in ℝ$
7		resubcl	$⊢ (A \in ℝ \land 1 \in ℝ) \to A - 1 \in ℝ$
8	4 6 7	sylancl	$⊢ φ \to A - 1 \in ℝ$
9		peano2re	$⊢ A \in ℝ \to A + 1 \in ℝ$
10	4 9	syl	$⊢ φ \to A + 1 \in ℝ$
11		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
12		ssid	$⊢ ℂ \subseteq ℂ$
13		fncpn	$⊢ ℂ \subseteq ℂ \to C^{n} (ℂ) Fn ℕ_{0}$
14	12 13	ax-mp	$⊢ C^{n} (ℂ) Fn ℕ_{0}$
15		1nn0	$⊢ 1 \in ℕ_{0}$
16		fnfvelrn	$⊢ (C^{n} (ℂ) Fn ℕ_{0} \land 1 \in ℕ_{0}) \to C^{n} (ℂ) (1) \in ran C^{n} (ℂ)$
17	14 15 16	mp2an	$⊢ C^{n} (ℂ) (1) \in ran C^{n} (ℂ)$
18		intss1	$⊢ C^{n} (ℂ) (1) \in ran C^{n} (ℂ) \to ⋂ ran C^{n} (ℂ) \subseteq C^{n} (ℂ) (1)$
19	17 18	ax-mp	$⊢ ⋂ ran C^{n} (ℂ) \subseteq C^{n} (ℂ) (1)$
20		plycpn	$⊢ F \in Poly (ℤ) \to F \in ⋂ ran C^{n} (ℂ)$
21	2 20	syl	$⊢ φ \to F \in ⋂ ran C^{n} (ℂ)$
22	19 21	sselid	$⊢ φ \to F \in C^{n} (ℂ) (1)$
23		cpnres	$⊢ (ℝ \in \{ℝ, ℂ\} \land F \in C^{n} (ℂ) (1)) \to {F ↾}_{ℝ} \in C^{n} (ℝ) (1)$
24	11 22 23	sylancr	$⊢ φ \to {F ↾}_{ℝ} \in C^{n} (ℝ) (1)$
25		df-ima	$⊢ F [ℝ] = ran ({F ↾}_{ℝ})$
26		zssre	$⊢ ℤ \subseteq ℝ$
27		ax-resscn	$⊢ ℝ \subseteq ℂ$
28		plyss	$⊢ (ℤ \subseteq ℝ \land ℝ \subseteq ℂ) \to Poly (ℤ) \subseteq Poly (ℝ)$
29	26 27 28	mp2an	$⊢ Poly (ℤ) \subseteq Poly (ℝ)$
30	29 2	sselid	$⊢ φ \to F \in Poly (ℝ)$
31		plyreres	$⊢ F \in Poly (ℝ) \to ({F ↾}_{ℝ}) : ℝ ⟶ ℝ$
32	30 31	syl	$⊢ φ \to ({F ↾}_{ℝ}) : ℝ ⟶ ℝ$
33	32	frnd	$⊢ φ \to ran ({F ↾}_{ℝ}) \subseteq ℝ$
34	25 33	eqsstrid	$⊢ φ \to F [ℝ] \subseteq ℝ$
35		iccssre	$⊢ (A - 1 \in ℝ \land A + 1 \in ℝ) \to [A - 1, A + 1] \subseteq ℝ$
36	8 10 35	syl2anc	$⊢ φ \to [A - 1, A + 1] \subseteq ℝ$
37	36 27	sstrdi	$⊢ φ \to [A - 1, A + 1] \subseteq ℂ$
38		plyf	$⊢ F \in Poly (ℤ) \to F : ℂ ⟶ ℂ$
39	2 38	syl	$⊢ φ \to F : ℂ ⟶ ℂ$
40	39	fdmd	$⊢ φ \to dom F = ℂ$
41	37 40	sseqtrrd	$⊢ φ \to [A - 1, A + 1] \subseteq dom F$
42	8 10 24 34 41	c1lip3	$⊢ φ \to \exists a \in ℝ \forall b \in [A - 1, A + 1] \forall c \in [A - 1, A + 1] \|F (c) - F (b)\| \leq a \|c - b\|$
43		simp2	$⊢ ((φ \land a \in ℝ) \land r \in ℝ \land \|A - r\| \leq 1) \to r \in ℝ$
44	43	recnd	$⊢ ((φ \land a \in ℝ) \land r \in ℝ \land \|A - r\| \leq 1) \to r \in ℂ$
45	4	adantr	$⊢ (φ \land a \in ℝ) \to A \in ℝ$
46	45	3ad2ant1	$⊢ ((φ \land a \in ℝ) \land r \in ℝ \land \|A - r\| \leq 1) \to A \in ℝ$
47	46	recnd	$⊢ ((φ \land a \in ℝ) \land r \in ℝ \land \|A - r\| \leq 1) \to A \in ℂ$
48	44 47	abssubd	$⊢ ((φ \land a \in ℝ) \land r \in ℝ \land \|A - r\| \leq 1) \to \|r - A\| = \|A - r\|$
49		simp3	$⊢ ((φ \land a \in ℝ) \land r \in ℝ \land \|A - r\| \leq 1) \to \|A - r\| \leq 1$
50	48 49	eqbrtrd	$⊢ ((φ \land a \in ℝ) \land r \in ℝ \land \|A - r\| \leq 1) \to \|r - A\| \leq 1$
51		1red	$⊢ ((φ \land a \in ℝ) \land r \in ℝ \land \|A - r\| \leq 1) \to 1 \in ℝ$
52		elicc4abs	$⊢ (A \in ℝ \land 1 \in ℝ \land r \in ℝ) \to (r \in [A - 1, A + 1] \leftrightarrow \|r - A\| \leq 1)$
53	46 51 43 52	syl3anc	$⊢ ((φ \land a \in ℝ) \land r \in ℝ \land \|A - r\| \leq 1) \to (r \in [A - 1, A + 1] \leftrightarrow \|r - A\| \leq 1)$
54	50 53	mpbird	$⊢ ((φ \land a \in ℝ) \land r \in ℝ \land \|A - r\| \leq 1) \to r \in [A - 1, A + 1]$
55	4	recnd	$⊢ φ \to A \in ℂ$
56	55	subidd	$⊢ φ \to A - A = 0$
57	56	fveq2d	$⊢ φ \to \|A - A\| = \|0\|$
58		abs0	$⊢ \|0\| = 0$
59		0le1	$⊢ 0 \leq 1$
60	58 59	eqbrtri	$⊢ \|0\| \leq 1$
61	57 60	eqbrtrdi	$⊢ φ \to \|A - A\| \leq 1$
62		1red	$⊢ φ \to 1 \in ℝ$
63		elicc4abs	$⊢ (A \in ℝ \land 1 \in ℝ \land A \in ℝ) \to (A \in [A - 1, A + 1] \leftrightarrow \|A - A\| \leq 1)$
64	4 62 4 63	syl3anc	$⊢ φ \to (A \in [A - 1, A + 1] \leftrightarrow \|A - A\| \leq 1)$
65	61 64	mpbird	$⊢ φ \to A \in [A - 1, A + 1]$
66	65	adantr	$⊢ (φ \land a \in ℝ) \to A \in [A - 1, A + 1]$
67	66	3ad2ant1	$⊢ ((φ \land a \in ℝ) \land r \in ℝ \land \|A - r\| \leq 1) \to A \in [A - 1, A + 1]$
68		fveq2	$⊢ b = r \to F (b) = F (r)$
69	68	oveq2d	$⊢ b = r \to F (c) - F (b) = F (c) - F (r)$
70	69	fveq2d	$⊢ b = r \to \|F (c) - F (b)\| = \|F (c) - F (r)\|$
71		oveq2	$⊢ b = r \to c - b = c - r$
72	71	fveq2d	$⊢ b = r \to \|c - b\| = \|c - r\|$
73	72	oveq2d	$⊢ b = r \to a \|c - b\| = a \|c - r\|$
74	70 73	breq12d	$⊢ b = r \to (\|F (c) - F (b)\| \leq a \|c - b\| \leftrightarrow \|F (c) - F (r)\| \leq a \|c - r\|)$
75		fveq2	$⊢ c = A \to F (c) = F (A)$
76	75	fvoveq1d	$⊢ c = A \to \|F (c) - F (r)\| = \|F (A) - F (r)\|$
77		fvoveq1	$⊢ c = A \to \|c - r\| = \|A - r\|$
78	77	oveq2d	$⊢ c = A \to a \|c - r\| = a \|A - r\|$
79	76 78	breq12d	$⊢ c = A \to (\|F (c) - F (r)\| \leq a \|c - r\| \leftrightarrow \|F (A) - F (r)\| \leq a \|A - r\|)$
80	74 79	rspc2v	$⊢ (r \in [A - 1, A + 1] \land A \in [A - 1, A + 1]) \to (\forall b \in [A - 1, A + 1] \forall c \in [A - 1, A + 1] \|F (c) - F (b)\| \leq a \|c - b\| \to \|F (A) - F (r)\| \leq a \|A - r\|)$
81	54 67 80	syl2anc	$⊢ ((φ \land a \in ℝ) \land r \in ℝ \land \|A - r\| \leq 1) \to (\forall b \in [A - 1, A + 1] \forall c \in [A - 1, A + 1] \|F (c) - F (b)\| \leq a \|c - b\| \to \|F (A) - F (r)\| \leq a \|A - r\|)$
82		simp1l	$⊢ ((φ \land a \in ℝ) \land r \in ℝ \land \|A - r\| \leq 1) \to φ$
83	82 5	syl	$⊢ ((φ \land a \in ℝ) \land r \in ℝ \land \|A - r\| \leq 1) \to F (A) = 0$
84		0cn	$⊢ 0 \in ℂ$
85	83 84	eqeltrdi	$⊢ ((φ \land a \in ℝ) \land r \in ℝ \land \|A - r\| \leq 1) \to F (A) \in ℂ$
86	39	adantr	$⊢ (φ \land a \in ℝ) \to F : ℂ ⟶ ℂ$
87	86	3ad2ant1	$⊢ ((φ \land a \in ℝ) \land r \in ℝ \land \|A - r\| \leq 1) \to F : ℂ ⟶ ℂ$
88	87 44	ffvelrnd	$⊢ ((φ \land a \in ℝ) \land r \in ℝ \land \|A - r\| \leq 1) \to F (r) \in ℂ$
89	85 88	abssubd	$⊢ ((φ \land a \in ℝ) \land r \in ℝ \land \|A - r\| \leq 1) \to \|F (A) - F (r)\| = \|F (r) - F (A)\|$
90	83	oveq2d	$⊢ ((φ \land a \in ℝ) \land r \in ℝ \land \|A - r\| \leq 1) \to F (r) - F (A) = F (r) - 0$
91	88	subid1d	$⊢ ((φ \land a \in ℝ) \land r \in ℝ \land \|A - r\| \leq 1) \to F (r) - 0 = F (r)$
92	90 91	eqtrd	$⊢ ((φ \land a \in ℝ) \land r \in ℝ \land \|A - r\| \leq 1) \to F (r) - F (A) = F (r)$
93	92	fveq2d	$⊢ ((φ \land a \in ℝ) \land r \in ℝ \land \|A - r\| \leq 1) \to \|F (r) - F (A)\| = \|F (r)\|$
94	89 93	eqtrd	$⊢ ((φ \land a \in ℝ) \land r \in ℝ \land \|A - r\| \leq 1) \to \|F (A) - F (r)\| = \|F (r)\|$
95	94	breq1d	$⊢ ((φ \land a \in ℝ) \land r \in ℝ \land \|A - r\| \leq 1) \to (\|F (A) - F (r)\| \leq a \|A - r\| \leftrightarrow \|F (r)\| \leq a \|A - r\|)$
96	81 95	sylibd	$⊢ ((φ \land a \in ℝ) \land r \in ℝ \land \|A - r\| \leq 1) \to (\forall b \in [A - 1, A + 1] \forall c \in [A - 1, A + 1] \|F (c) - F (b)\| \leq a \|c - b\| \to \|F (r)\| \leq a \|A - r\|)$
97	96	3exp	$⊢ (φ \land a \in ℝ) \to (r \in ℝ \to (\|A - r\| \leq 1 \to (\forall b \in [A - 1, A + 1] \forall c \in [A - 1, A + 1] \|F (c) - F (b)\| \leq a \|c - b\| \to \|F (r)\| \leq a \|A - r\|)))$
98	97	com34	$⊢ (φ \land a \in ℝ) \to (r \in ℝ \to (\forall b \in [A - 1, A + 1] \forall c \in [A - 1, A + 1] \|F (c) - F (b)\| \leq a \|c - b\| \to (\|A - r\| \leq 1 \to \|F (r)\| \leq a \|A - r\|)))$
99	98	com23	$⊢ (φ \land a \in ℝ) \to (\forall b \in [A - 1, A + 1] \forall c \in [A - 1, A + 1] \|F (c) - F (b)\| \leq a \|c - b\| \to (r \in ℝ \to (\|A - r\| \leq 1 \to \|F (r)\| \leq a \|A - r\|)))$
100	99	ralrimdv	$⊢ (φ \land a \in ℝ) \to (\forall b \in [A - 1, A + 1] \forall c \in [A - 1, A + 1] \|F (c) - F (b)\| \leq a \|c - b\| \to \forall r \in ℝ (\|A - r\| \leq 1 \to \|F (r)\| \leq a \|A - r\|))$
101	100	reximdva	$⊢ φ \to (\exists a \in ℝ \forall b \in [A - 1, A + 1] \forall c \in [A - 1, A + 1] \|F (c) - F (b)\| \leq a \|c - b\| \to \exists a \in ℝ \forall r \in ℝ (\|A - r\| \leq 1 \to \|F (r)\| \leq a \|A - r\|))$
102	42 101	mpd	$⊢ φ \to \exists a \in ℝ \forall r \in ℝ (\|A - r\| \leq 1 \to \|F (r)\| \leq a \|A - r\|)$
103		1rp	$⊢ 1 \in ℝ^{+}$
104	103	a1i	$⊢ ((φ \land a \in ℝ) \land a = 0) \to 1 \in ℝ^{+}$
105		recn	$⊢ a \in ℝ \to a \in ℂ$
106	105	adantl	$⊢ (φ \land a \in ℝ) \to a \in ℂ$
107		neqne	$⊢ \neg a = 0 \to a \neq 0$
108		absrpcl	$⊢ (a \in ℂ \land a \neq 0) \to \|a\| \in ℝ^{+}$
109	106 107 108	syl2an	$⊢ ((φ \land a \in ℝ) \land \neg a = 0) \to \|a\| \in ℝ^{+}$
110	109	rpreccld	$⊢ ((φ \land a \in ℝ) \land \neg a = 0) \to \frac{1}{\|a\|} \in ℝ^{+}$
111	104 110	ifclda	$⊢ (φ \land a \in ℝ) \to if (a = 0, 1, \frac{1}{\|a\|}) \in ℝ^{+}$
112		eqid	$⊢ if (a = 0, 1, \frac{1}{\|a\|}) = if (a = 0, 1, \frac{1}{\|a\|})$
113		eqif	$⊢ if (a = 0, 1, \frac{1}{\|a\|}) = if (a = 0, 1, \frac{1}{\|a\|}) \leftrightarrow ((a = 0 \land if (a = 0, 1, \frac{1}{\|a\|}) = 1) \lor (\neg a = 0 \land if (a = 0, 1, \frac{1}{\|a\|}) = \frac{1}{\|a\|}))$
114	112 113	mpbi	$⊢ ((a = 0 \land if (a = 0, 1, \frac{1}{\|a\|}) = 1) \lor (\neg a = 0 \land if (a = 0, 1, \frac{1}{\|a\|}) = \frac{1}{\|a\|}))$
115		simplrr	$⊢ (((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \land a = 0) \to \|F (r)\| \leq a \|A - r\|$
116		oveq1	$⊢ a = 0 \to a \|A - r\| = 0 \cdot \|A - r\|$
117	116	adantl	$⊢ (((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \land a = 0) \to a \|A - r\| = 0 \cdot \|A - r\|$
118	4	ad2antrr	$⊢ ((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \to A \in ℝ$
119		simprl	$⊢ ((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \to r \in ℝ$
120	118 119	resubcld	$⊢ ((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \to A - r \in ℝ$
121	120	recnd	$⊢ ((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \to A - r \in ℂ$
122	121	abscld	$⊢ ((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \to \|A - r\| \in ℝ$
123	122	recnd	$⊢ ((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \to \|A - r\| \in ℂ$
124	123	adantr	$⊢ (((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \land a = 0) \to \|A - r\| \in ℂ$
125	124	mul02d	$⊢ (((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \land a = 0) \to 0 \cdot \|A - r\| = 0$
126	117 125	eqtrd	$⊢ (((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \land a = 0) \to a \|A - r\| = 0$
127	115 126	breqtrd	$⊢ (((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \land a = 0) \to \|F (r)\| \leq 0$
128	39	ad2antrr	$⊢ ((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \to F : ℂ ⟶ ℂ$
129	119	recnd	$⊢ ((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \to r \in ℂ$
130	128 129	ffvelrnd	$⊢ ((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \to F (r) \in ℂ$
131	130	adantr	$⊢ (((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \land a = 0) \to F (r) \in ℂ$
132	131	absge0d	$⊢ (((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \land a = 0) \to 0 \leq \|F (r)\|$
133	130	abscld	$⊢ ((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \to \|F (r)\| \in ℝ$
134	133	adantr	$⊢ (((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \land a = 0) \to \|F (r)\| \in ℝ$
135		0re	$⊢ 0 \in ℝ$
136		letri3	$⊢ (\|F (r)\| \in ℝ \land 0 \in ℝ) \to (\|F (r)\| = 0 \leftrightarrow (\|F (r)\| \leq 0 \land 0 \leq \|F (r)\|))$
137	134 135 136	sylancl	$⊢ (((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \land a = 0) \to (\|F (r)\| = 0 \leftrightarrow (\|F (r)\| \leq 0 \land 0 \leq \|F (r)\|))$
138	127 132 137	mpbir2and	$⊢ (((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \land a = 0) \to \|F (r)\| = 0$
139	138	oveq2d	$⊢ (((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \land a = 0) \to 1 \|F (r)\| = 1 \cdot 0$
140		ax-1cn	$⊢ 1 \in ℂ$
141	140	mul01i	$⊢ 1 \cdot 0 = 0$
142	139 141	eqtrdi	$⊢ (((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \land a = 0) \to 1 \|F (r)\| = 0$
143	121	adantr	$⊢ (((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \land a = 0) \to A - r \in ℂ$
144	143	absge0d	$⊢ (((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \land a = 0) \to 0 \leq \|A - r\|$
145	142 144	eqbrtrd	$⊢ (((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \land a = 0) \to 1 \|F (r)\| \leq \|A - r\|$
146		oveq1	$⊢ if (a = 0, 1, \frac{1}{\|a\|}) = 1 \to if (a = 0, 1, \frac{1}{\|a\|}) \|F (r)\| = 1 \|F (r)\|$
147	146	breq1d	$⊢ if (a = 0, 1, \frac{1}{\|a\|}) = 1 \to (if (a = 0, 1, \frac{1}{\|a\|}) \|F (r)\| \leq \|A - r\| \leftrightarrow 1 \|F (r)\| \leq \|A - r\|)$
148	145 147	syl5ibrcom	$⊢ (((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \land a = 0) \to (if (a = 0, 1, \frac{1}{\|a\|}) = 1 \to if (a = 0, 1, \frac{1}{\|a\|}) \|F (r)\| \leq \|A - r\|)$
149	148	expimpd	$⊢ ((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \to ((a = 0 \land if (a = 0, 1, \frac{1}{\|a\|}) = 1) \to if (a = 0, 1, \frac{1}{\|a\|}) \|F (r)\| \leq \|A - r\|)$
150		df-ne	$⊢ a \neq 0 \leftrightarrow \neg a = 0$
151	133	adantr	$⊢ (((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \land a \neq 0) \to \|F (r)\| \in ℝ$
152	151	recnd	$⊢ (((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \land a \neq 0) \to \|F (r)\| \in ℂ$
153		simpllr	$⊢ (((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \land a \neq 0) \to a \in ℝ$
154	153	recnd	$⊢ (((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \land a \neq 0) \to a \in ℂ$
155	154 108	sylancom	$⊢ (((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \land a \neq 0) \to \|a\| \in ℝ^{+}$
156	155	rpcnne0d	$⊢ (((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \land a \neq 0) \to (\|a\| \in ℂ \land \|a\| \neq 0)$
157		divrec2	$⊢ (\|F (r)\| \in ℂ \land \|a\| \in ℂ \land \|a\| \neq 0) \to \frac{\|F (r)\|}{\|a\|} = (\frac{1}{\|a\|}) \|F (r)\|$
158	157	3expb	$⊢ (\|F (r)\| \in ℂ \land (\|a\| \in ℂ \land \|a\| \neq 0)) \to \frac{\|F (r)\|}{\|a\|} = (\frac{1}{\|a\|}) \|F (r)\|$
159	152 156 158	syl2anc	$⊢ (((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \land a \neq 0) \to \frac{\|F (r)\|}{\|a\|} = (\frac{1}{\|a\|}) \|F (r)\|$
160		simplr	$⊢ ((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \to a \in ℝ$
161	160 122	remulcld	$⊢ ((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \to a \|A - r\| \in ℝ$
162	160	recnd	$⊢ ((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \to a \in ℂ$
163	162	abscld	$⊢ ((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \to \|a\| \in ℝ$
164	163 122	remulcld	$⊢ ((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \to \|a\| \|A - r\| \in ℝ$
165		simprr	$⊢ ((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \to \|F (r)\| \leq a \|A - r\|$
166	121	absge0d	$⊢ ((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \to 0 \leq \|A - r\|$
167		leabs	$⊢ a \in ℝ \to a \leq \|a\|$
168	167	ad2antlr	$⊢ ((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \to a \leq \|a\|$
169	160 163 122 166 168	lemul1ad	$⊢ ((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \to a \|A - r\| \leq \|a\| \|A - r\|$
170	133 161 164 165 169	letrd	$⊢ ((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \to \|F (r)\| \leq \|a\| \|A - r\|$
171	170	adantr	$⊢ (((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \land a \neq 0) \to \|F (r)\| \leq \|a\| \|A - r\|$
172	122	adantr	$⊢ (((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \land a \neq 0) \to \|A - r\| \in ℝ$
173	151 172 155	ledivmuld	$⊢ (((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \land a \neq 0) \to (\frac{\|F (r)\|}{\|a\|} \leq \|A - r\| \leftrightarrow \|F (r)\| \leq \|a\| \|A - r\|)$
174	171 173	mpbird	$⊢ (((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \land a \neq 0) \to \frac{\|F (r)\|}{\|a\|} \leq \|A - r\|$
175	159 174	eqbrtrrd	$⊢ (((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \land a \neq 0) \to (\frac{1}{\|a\|}) \|F (r)\| \leq \|A - r\|$
176	150 175	sylan2br	$⊢ (((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \land \neg a = 0) \to (\frac{1}{\|a\|}) \|F (r)\| \leq \|A - r\|$
177		oveq1	$⊢ if (a = 0, 1, \frac{1}{\|a\|}) = \frac{1}{\|a\|} \to if (a = 0, 1, \frac{1}{\|a\|}) \|F (r)\| = (\frac{1}{\|a\|}) \|F (r)\|$
178	177	breq1d	$⊢ if (a = 0, 1, \frac{1}{\|a\|}) = \frac{1}{\|a\|} \to (if (a = 0, 1, \frac{1}{\|a\|}) \|F (r)\| \leq \|A - r\| \leftrightarrow (\frac{1}{\|a\|}) \|F (r)\| \leq \|A - r\|)$
179	176 178	syl5ibrcom	$⊢ (((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \land \neg a = 0) \to (if (a = 0, 1, \frac{1}{\|a\|}) = \frac{1}{\|a\|} \to if (a = 0, 1, \frac{1}{\|a\|}) \|F (r)\| \leq \|A - r\|)$
180	179	expimpd	$⊢ ((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \to ((\neg a = 0 \land if (a = 0, 1, \frac{1}{\|a\|}) = \frac{1}{\|a\|}) \to if (a = 0, 1, \frac{1}{\|a\|}) \|F (r)\| \leq \|A - r\|)$
181	149 180	jaod	$⊢ ((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \to (((a = 0 \land if (a = 0, 1, \frac{1}{\|a\|}) = 1) \lor (\neg a = 0 \land if (a = 0, 1, \frac{1}{\|a\|}) = \frac{1}{\|a\|})) \to if (a = 0, 1, \frac{1}{\|a\|}) \|F (r)\| \leq \|A - r\|)$
182	114 181	mpi	$⊢ ((φ \land a \in ℝ) \land (r \in ℝ \land \|F (r)\| \leq a \|A - r\|)) \to if (a = 0, 1, \frac{1}{\|a\|}) \|F (r)\| \leq \|A - r\|$
183	182	expr	$⊢ ((φ \land a \in ℝ) \land r \in ℝ) \to (\|F (r)\| \leq a \|A - r\| \to if (a = 0, 1, \frac{1}{\|a\|}) \|F (r)\| \leq \|A - r\|)$
184	183	imim2d	$⊢ ((φ \land a \in ℝ) \land r \in ℝ) \to ((\|A - r\| \leq 1 \to \|F (r)\| \leq a \|A - r\|) \to (\|A - r\| \leq 1 \to if (a = 0, 1, \frac{1}{\|a\|}) \|F (r)\| \leq \|A - r\|))$
185	184	ralimdva	$⊢ (φ \land a \in ℝ) \to (\forall r \in ℝ (\|A - r\| \leq 1 \to \|F (r)\| \leq a \|A - r\|) \to \forall r \in ℝ (\|A - r\| \leq 1 \to if (a = 0, 1, \frac{1}{\|a\|}) \|F (r)\| \leq \|A - r\|))$
186		oveq1	$⊢ x = if (a = 0, 1, \frac{1}{\|a\|}) \to x \|F (r)\| = if (a = 0, 1, \frac{1}{\|a\|}) \|F (r)\|$
187	186	breq1d	$⊢ x = if (a = 0, 1, \frac{1}{\|a\|}) \to (x \|F (r)\| \leq \|A - r\| \leftrightarrow if (a = 0, 1, \frac{1}{\|a\|}) \|F (r)\| \leq \|A - r\|)$
188	187	imbi2d	$⊢ x = if (a = 0, 1, \frac{1}{\|a\|}) \to ((\|A - r\| \leq 1 \to x \|F (r)\| \leq \|A - r\|) \leftrightarrow (\|A - r\| \leq 1 \to if (a = 0, 1, \frac{1}{\|a\|}) \|F (r)\| \leq \|A - r\|))$
189	188	ralbidv	$⊢ x = if (a = 0, 1, \frac{1}{\|a\|}) \to (\forall r \in ℝ (\|A - r\| \leq 1 \to x \|F (r)\| \leq \|A - r\|) \leftrightarrow \forall r \in ℝ (\|A - r\| \leq 1 \to if (a = 0, 1, \frac{1}{\|a\|}) \|F (r)\| \leq \|A - r\|))$
190	189	rspcev	$⊢ (if (a = 0, 1, \frac{1}{\|a\|}) \in ℝ^{+} \land \forall r \in ℝ (\|A - r\| \leq 1 \to if (a = 0, 1, \frac{1}{\|a\|}) \|F (r)\| \leq \|A - r\|)) \to \exists x \in ℝ^{+} \forall r \in ℝ (\|A - r\| \leq 1 \to x \|F (r)\| \leq \|A - r\|)$
191	111 185 190	syl6an	$⊢ (φ \land a \in ℝ) \to (\forall r \in ℝ (\|A - r\| \leq 1 \to \|F (r)\| \leq a \|A - r\|) \to \exists x \in ℝ^{+} \forall r \in ℝ (\|A - r\| \leq 1 \to x \|F (r)\| \leq \|A - r\|))$
192	191	rexlimdva	$⊢ φ \to (\exists a \in ℝ \forall r \in ℝ (\|A - r\| \leq 1 \to \|F (r)\| \leq a \|A - r\|) \to \exists x \in ℝ^{+} \forall r \in ℝ (\|A - r\| \leq 1 \to x \|F (r)\| \leq \|A - r\|))$
193	102 192	mpd	$⊢ φ \to \exists x \in ℝ^{+} \forall r \in ℝ (\|A - r\| \leq 1 \to x \|F (r)\| \leq \|A - r\|)$

Metamath Proof Explorer

Theorem aalioulem3

Proof