Metamath Proof Explorer

Theorem aalioulem3

Description: Lemma for aaliou . (Contributed by Stefan O'Rear, 15-Nov-2014)

Ref Expression
Hypotheses aalioulem2.a ⊢N=deg⁡F
aalioulem2.b ⊢φ→F∈Poly⁡ℤ
aalioulem2.c ⊢φ→N∈ℕ
aalioulem2.d ⊢φ→A∈ℝ
aalioulem3.e ⊢φ→F⁡A=0
Assertion aalioulem3 ⊢φ→∃x∈ℝ+∀r∈ℝA−r≤1→x⁢F⁡r≤A−r

Proof

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