MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ftalem7 Structured version   Visualization version   GIF version

Theorem ftalem7 24996
Description: Lemma for fta 24997. Shift the minimum away from zero by a change of variables. (Contributed by Mario Carneiro, 14-Sep-2014.)
Hypotheses
Ref Expression
ftalem.1 𝐴 = (coeff‘𝐹)
ftalem.2 𝑁 = (deg‘𝐹)
ftalem.3 (𝜑𝐹 ∈ (Poly‘𝑆))
ftalem.4 (𝜑𝑁 ∈ ℕ)
ftalem7.5 (𝜑𝑋 ∈ ℂ)
ftalem7.6 (𝜑 → (𝐹𝑋) ≠ 0)
Assertion
Ref Expression
ftalem7 (𝜑 → ¬ ∀𝑥 ∈ ℂ (abs‘(𝐹𝑋)) ≤ (abs‘(𝐹𝑥)))
Distinct variable groups:   𝑥,𝐴   𝑥,𝑁   𝑥,𝐹   𝜑,𝑥   𝑥,𝑋
Allowed substitution hint:   𝑆(𝑥)

Proof of Theorem ftalem7
Dummy variables 𝑧 𝑤 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2752 . . . 4 (coeff‘(𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))) = (coeff‘(𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋))))
2 eqid 2752 . . . 4 (deg‘(𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))) = (deg‘(𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋))))
3 simpr 479 . . . . . . 7 ((𝜑𝑧 ∈ ℂ) → 𝑧 ∈ ℂ)
4 ftalem7.5 . . . . . . . 8 (𝜑𝑋 ∈ ℂ)
54adantr 472 . . . . . . 7 ((𝜑𝑧 ∈ ℂ) → 𝑋 ∈ ℂ)
63, 5addcld 10243 . . . . . 6 ((𝜑𝑧 ∈ ℂ) → (𝑧 + 𝑋) ∈ ℂ)
7 cnex 10201 . . . . . . . . 9 ℂ ∈ V
87a1i 11 . . . . . . . 8 (𝜑 → ℂ ∈ V)
94negcld 10563 . . . . . . . . 9 (𝜑 → -𝑋 ∈ ℂ)
109adantr 472 . . . . . . . 8 ((𝜑𝑧 ∈ ℂ) → -𝑋 ∈ ℂ)
11 df-idp 24136 . . . . . . . . . 10 Xp = ( I ↾ ℂ)
12 mptresid 5606 . . . . . . . . . 10 (𝑧 ∈ ℂ ↦ 𝑧) = ( I ↾ ℂ)
1311, 12eqtr4i 2777 . . . . . . . . 9 Xp = (𝑧 ∈ ℂ ↦ 𝑧)
1413a1i 11 . . . . . . . 8 (𝜑Xp = (𝑧 ∈ ℂ ↦ 𝑧))
15 fconstmpt 5312 . . . . . . . . 9 (ℂ × {-𝑋}) = (𝑧 ∈ ℂ ↦ -𝑋)
1615a1i 11 . . . . . . . 8 (𝜑 → (ℂ × {-𝑋}) = (𝑧 ∈ ℂ ↦ -𝑋))
178, 3, 10, 14, 16offval2 7071 . . . . . . 7 (𝜑 → (Xp𝑓 − (ℂ × {-𝑋})) = (𝑧 ∈ ℂ ↦ (𝑧 − -𝑋)))
18 id 22 . . . . . . . . 9 (𝑧 ∈ ℂ → 𝑧 ∈ ℂ)
19 subneg 10514 . . . . . . . . 9 ((𝑧 ∈ ℂ ∧ 𝑋 ∈ ℂ) → (𝑧 − -𝑋) = (𝑧 + 𝑋))
2018, 4, 19syl2anr 496 . . . . . . . 8 ((𝜑𝑧 ∈ ℂ) → (𝑧 − -𝑋) = (𝑧 + 𝑋))
2120mpteq2dva 4888 . . . . . . 7 (𝜑 → (𝑧 ∈ ℂ ↦ (𝑧 − -𝑋)) = (𝑧 ∈ ℂ ↦ (𝑧 + 𝑋)))
2217, 21eqtrd 2786 . . . . . 6 (𝜑 → (Xp𝑓 − (ℂ × {-𝑋})) = (𝑧 ∈ ℂ ↦ (𝑧 + 𝑋)))
23 ftalem.3 . . . . . . . 8 (𝜑𝐹 ∈ (Poly‘𝑆))
24 plyf 24145 . . . . . . . 8 (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ)
2523, 24syl 17 . . . . . . 7 (𝜑𝐹:ℂ⟶ℂ)
2625feqmptd 6403 . . . . . 6 (𝜑𝐹 = (𝑦 ∈ ℂ ↦ (𝐹𝑦)))
27 fveq2 6344 . . . . . 6 (𝑦 = (𝑧 + 𝑋) → (𝐹𝑦) = (𝐹‘(𝑧 + 𝑋)))
286, 22, 26, 27fmptco 6551 . . . . 5 (𝜑 → (𝐹 ∘ (Xp𝑓 − (ℂ × {-𝑋}))) = (𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋))))
29 plyssc 24147 . . . . . . 7 (Poly‘𝑆) ⊆ (Poly‘ℂ)
3029, 23sseldi 3734 . . . . . 6 (𝜑𝐹 ∈ (Poly‘ℂ))
31 eqid 2752 . . . . . . . . 9 (Xp𝑓 − (ℂ × {-𝑋})) = (Xp𝑓 − (ℂ × {-𝑋}))
3231plyremlem 24250 . . . . . . . 8 (-𝑋 ∈ ℂ → ((Xp𝑓 − (ℂ × {-𝑋})) ∈ (Poly‘ℂ) ∧ (deg‘(Xp𝑓 − (ℂ × {-𝑋}))) = 1 ∧ ((Xp𝑓 − (ℂ × {-𝑋})) “ {0}) = {-𝑋}))
339, 32syl 17 . . . . . . 7 (𝜑 → ((Xp𝑓 − (ℂ × {-𝑋})) ∈ (Poly‘ℂ) ∧ (deg‘(Xp𝑓 − (ℂ × {-𝑋}))) = 1 ∧ ((Xp𝑓 − (ℂ × {-𝑋})) “ {0}) = {-𝑋}))
3433simp1d 1136 . . . . . 6 (𝜑 → (Xp𝑓 − (ℂ × {-𝑋})) ∈ (Poly‘ℂ))
35 addcl 10202 . . . . . . 7 ((𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝑧 + 𝑤) ∈ ℂ)
3635adantl 473 . . . . . 6 ((𝜑 ∧ (𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ)) → (𝑧 + 𝑤) ∈ ℂ)
37 mulcl 10204 . . . . . . 7 ((𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝑧 · 𝑤) ∈ ℂ)
3837adantl 473 . . . . . 6 ((𝜑 ∧ (𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ)) → (𝑧 · 𝑤) ∈ ℂ)
3930, 34, 36, 38plyco 24188 . . . . 5 (𝜑 → (𝐹 ∘ (Xp𝑓 − (ℂ × {-𝑋}))) ∈ (Poly‘ℂ))
4028, 39eqeltrrd 2832 . . . 4 (𝜑 → (𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋))) ∈ (Poly‘ℂ))
4128fveq2d 6348 . . . . 5 (𝜑 → (deg‘(𝐹 ∘ (Xp𝑓 − (ℂ × {-𝑋})))) = (deg‘(𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))))
42 ftalem.2 . . . . . . 7 𝑁 = (deg‘𝐹)
43 eqid 2752 . . . . . . 7 (deg‘(Xp𝑓 − (ℂ × {-𝑋}))) = (deg‘(Xp𝑓 − (ℂ × {-𝑋})))
4442, 43, 30, 34dgrco 24222 . . . . . 6 (𝜑 → (deg‘(𝐹 ∘ (Xp𝑓 − (ℂ × {-𝑋})))) = (𝑁 · (deg‘(Xp𝑓 − (ℂ × {-𝑋})))))
45 ftalem.4 . . . . . . 7 (𝜑𝑁 ∈ ℕ)
4633simp2d 1137 . . . . . . . 8 (𝜑 → (deg‘(Xp𝑓 − (ℂ × {-𝑋}))) = 1)
47 1nn 11215 . . . . . . . 8 1 ∈ ℕ
4846, 47syl6eqel 2839 . . . . . . 7 (𝜑 → (deg‘(Xp𝑓 − (ℂ × {-𝑋}))) ∈ ℕ)
4945, 48nnmulcld 11252 . . . . . 6 (𝜑 → (𝑁 · (deg‘(Xp𝑓 − (ℂ × {-𝑋})))) ∈ ℕ)
5044, 49eqeltrd 2831 . . . . 5 (𝜑 → (deg‘(𝐹 ∘ (Xp𝑓 − (ℂ × {-𝑋})))) ∈ ℕ)
5141, 50eqeltrrd 2832 . . . 4 (𝜑 → (deg‘(𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))) ∈ ℕ)
52 0cn 10216 . . . . . . 7 0 ∈ ℂ
53 oveq1 6812 . . . . . . . . 9 (𝑧 = 0 → (𝑧 + 𝑋) = (0 + 𝑋))
5453fveq2d 6348 . . . . . . . 8 (𝑧 = 0 → (𝐹‘(𝑧 + 𝑋)) = (𝐹‘(0 + 𝑋)))
55 eqid 2752 . . . . . . . 8 (𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋))) = (𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))
56 fvex 6354 . . . . . . . 8 (𝐹‘(0 + 𝑋)) ∈ V
5754, 55, 56fvmpt 6436 . . . . . . 7 (0 ∈ ℂ → ((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘0) = (𝐹‘(0 + 𝑋)))
5852, 57ax-mp 5 . . . . . 6 ((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘0) = (𝐹‘(0 + 𝑋))
594addid2d 10421 . . . . . . 7 (𝜑 → (0 + 𝑋) = 𝑋)
6059fveq2d 6348 . . . . . 6 (𝜑 → (𝐹‘(0 + 𝑋)) = (𝐹𝑋))
6158, 60syl5eq 2798 . . . . 5 (𝜑 → ((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘0) = (𝐹𝑋))
62 ftalem7.6 . . . . 5 (𝜑 → (𝐹𝑋) ≠ 0)
6361, 62eqnetrd 2991 . . . 4 (𝜑 → ((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘0) ≠ 0)
641, 2, 40, 51, 63ftalem6 24995 . . 3 (𝜑 → ∃𝑦 ∈ ℂ (abs‘((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘𝑦)) < (abs‘((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘0)))
65 id 22 . . . . . 6 (𝑦 ∈ ℂ → 𝑦 ∈ ℂ)
66 addcl 10202 . . . . . 6 ((𝑦 ∈ ℂ ∧ 𝑋 ∈ ℂ) → (𝑦 + 𝑋) ∈ ℂ)
6765, 4, 66syl2anr 496 . . . . 5 ((𝜑𝑦 ∈ ℂ) → (𝑦 + 𝑋) ∈ ℂ)
68 oveq1 6812 . . . . . . . . . . . 12 (𝑧 = 𝑦 → (𝑧 + 𝑋) = (𝑦 + 𝑋))
6968fveq2d 6348 . . . . . . . . . . 11 (𝑧 = 𝑦 → (𝐹‘(𝑧 + 𝑋)) = (𝐹‘(𝑦 + 𝑋)))
70 fvex 6354 . . . . . . . . . . 11 (𝐹‘(𝑦 + 𝑋)) ∈ V
7169, 55, 70fvmpt 6436 . . . . . . . . . 10 (𝑦 ∈ ℂ → ((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘𝑦) = (𝐹‘(𝑦 + 𝑋)))
7271adantl 473 . . . . . . . . 9 ((𝜑𝑦 ∈ ℂ) → ((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘𝑦) = (𝐹‘(𝑦 + 𝑋)))
7372fveq2d 6348 . . . . . . . 8 ((𝜑𝑦 ∈ ℂ) → (abs‘((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘𝑦)) = (abs‘(𝐹‘(𝑦 + 𝑋))))
7461adantr 472 . . . . . . . . 9 ((𝜑𝑦 ∈ ℂ) → ((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘0) = (𝐹𝑋))
7574fveq2d 6348 . . . . . . . 8 ((𝜑𝑦 ∈ ℂ) → (abs‘((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘0)) = (abs‘(𝐹𝑋)))
7673, 75breq12d 4809 . . . . . . 7 ((𝜑𝑦 ∈ ℂ) → ((abs‘((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘𝑦)) < (abs‘((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘0)) ↔ (abs‘(𝐹‘(𝑦 + 𝑋))) < (abs‘(𝐹𝑋))))
7725adantr 472 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℂ) → 𝐹:ℂ⟶ℂ)
7877, 67ffvelrnd 6515 . . . . . . . . 9 ((𝜑𝑦 ∈ ℂ) → (𝐹‘(𝑦 + 𝑋)) ∈ ℂ)
7978abscld 14366 . . . . . . . 8 ((𝜑𝑦 ∈ ℂ) → (abs‘(𝐹‘(𝑦 + 𝑋))) ∈ ℝ)
8025, 4ffvelrnd 6515 . . . . . . . . . 10 (𝜑 → (𝐹𝑋) ∈ ℂ)
8180abscld 14366 . . . . . . . . 9 (𝜑 → (abs‘(𝐹𝑋)) ∈ ℝ)
8281adantr 472 . . . . . . . 8 ((𝜑𝑦 ∈ ℂ) → (abs‘(𝐹𝑋)) ∈ ℝ)
8379, 82ltnled 10368 . . . . . . 7 ((𝜑𝑦 ∈ ℂ) → ((abs‘(𝐹‘(𝑦 + 𝑋))) < (abs‘(𝐹𝑋)) ↔ ¬ (abs‘(𝐹𝑋)) ≤ (abs‘(𝐹‘(𝑦 + 𝑋)))))
8476, 83bitrd 268 . . . . . 6 ((𝜑𝑦 ∈ ℂ) → ((abs‘((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘𝑦)) < (abs‘((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘0)) ↔ ¬ (abs‘(𝐹𝑋)) ≤ (abs‘(𝐹‘(𝑦 + 𝑋)))))
8584biimpd 219 . . . . 5 ((𝜑𝑦 ∈ ℂ) → ((abs‘((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘𝑦)) < (abs‘((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘0)) → ¬ (abs‘(𝐹𝑋)) ≤ (abs‘(𝐹‘(𝑦 + 𝑋)))))
86 fveq2 6344 . . . . . . . . 9 (𝑥 = (𝑦 + 𝑋) → (𝐹𝑥) = (𝐹‘(𝑦 + 𝑋)))
8786fveq2d 6348 . . . . . . . 8 (𝑥 = (𝑦 + 𝑋) → (abs‘(𝐹𝑥)) = (abs‘(𝐹‘(𝑦 + 𝑋))))
8887breq2d 4808 . . . . . . 7 (𝑥 = (𝑦 + 𝑋) → ((abs‘(𝐹𝑋)) ≤ (abs‘(𝐹𝑥)) ↔ (abs‘(𝐹𝑋)) ≤ (abs‘(𝐹‘(𝑦 + 𝑋)))))
8988notbid 307 . . . . . 6 (𝑥 = (𝑦 + 𝑋) → (¬ (abs‘(𝐹𝑋)) ≤ (abs‘(𝐹𝑥)) ↔ ¬ (abs‘(𝐹𝑋)) ≤ (abs‘(𝐹‘(𝑦 + 𝑋)))))
9089rspcev 3441 . . . . 5 (((𝑦 + 𝑋) ∈ ℂ ∧ ¬ (abs‘(𝐹𝑋)) ≤ (abs‘(𝐹‘(𝑦 + 𝑋)))) → ∃𝑥 ∈ ℂ ¬ (abs‘(𝐹𝑋)) ≤ (abs‘(𝐹𝑥)))
9167, 85, 90syl6an 569 . . . 4 ((𝜑𝑦 ∈ ℂ) → ((abs‘((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘𝑦)) < (abs‘((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘0)) → ∃𝑥 ∈ ℂ ¬ (abs‘(𝐹𝑋)) ≤ (abs‘(𝐹𝑥))))
9291rexlimdva 3161 . . 3 (𝜑 → (∃𝑦 ∈ ℂ (abs‘((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘𝑦)) < (abs‘((𝑧 ∈ ℂ ↦ (𝐹‘(𝑧 + 𝑋)))‘0)) → ∃𝑥 ∈ ℂ ¬ (abs‘(𝐹𝑋)) ≤ (abs‘(𝐹𝑥))))
9364, 92mpd 15 . 2 (𝜑 → ∃𝑥 ∈ ℂ ¬ (abs‘(𝐹𝑋)) ≤ (abs‘(𝐹𝑥)))
94 rexnal 3125 . 2 (∃𝑥 ∈ ℂ ¬ (abs‘(𝐹𝑋)) ≤ (abs‘(𝐹𝑥)) ↔ ¬ ∀𝑥 ∈ ℂ (abs‘(𝐹𝑋)) ≤ (abs‘(𝐹𝑥)))
9593, 94sylib 208 1 (𝜑 → ¬ ∀𝑥 ∈ ℂ (abs‘(𝐹𝑋)) ≤ (abs‘(𝐹𝑥)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383  w3a 1072   = wceq 1624  wcel 2131  wne 2924  wral 3042  wrex 3043  Vcvv 3332  {csn 4313   class class class wbr 4796  cmpt 4873   I cid 5165   × cxp 5256  ccnv 5257  cres 5260  cima 5261  ccom 5262  wf 6037  cfv 6041  (class class class)co 6805  𝑓 cof 7052  cc 10118  cr 10119  0cc0 10120  1c1 10121   + caddc 10123   · cmul 10125   < clt 10258  cle 10259  cmin 10450  -cneg 10451  cn 11204  abscabs 14165  Polycply 24131  Xpcidp 24132  coeffccoe 24133  degcdgr 24134
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-8 2133  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-rep 4915  ax-sep 4925  ax-nul 4933  ax-pow 4984  ax-pr 5047  ax-un 7106  ax-inf2 8703  ax-cnex 10176  ax-resscn 10177  ax-1cn 10178  ax-icn 10179  ax-addcl 10180  ax-addrcl 10181  ax-mulcl 10182  ax-mulrcl 10183  ax-mulcom 10184  ax-addass 10185  ax-mulass 10186  ax-distr 10187  ax-i2m1 10188  ax-1ne0 10189  ax-1rid 10190  ax-rnegex 10191  ax-rrecex 10192  ax-cnre 10193  ax-pre-lttri 10194  ax-pre-lttrn 10195  ax-pre-ltadd 10196  ax-pre-mulgt0 10197  ax-pre-sup 10198  ax-addf 10199  ax-mulf 10200
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1627  df-fal 1630  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-nel 3028  df-ral 3047  df-rex 3048  df-reu 3049  df-rmo 3050  df-rab 3051  df-v 3334  df-sbc 3569  df-csb 3667  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-pss 3723  df-nul 4051  df-if 4223  df-pw 4296  df-sn 4314  df-pr 4316  df-tp 4318  df-op 4320  df-uni 4581  df-int 4620  df-iun 4666  df-iin 4667  df-br 4797  df-opab 4857  df-mpt 4874  df-tr 4897  df-id 5166  df-eprel 5171  df-po 5179  df-so 5180  df-fr 5217  df-se 5218  df-we 5219  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-rn 5269  df-res 5270  df-ima 5271  df-pred 5833  df-ord 5879  df-on 5880  df-lim 5881  df-suc 5882  df-iota 6004  df-fun 6043  df-fn 6044  df-f 6045  df-f1 6046  df-fo 6047  df-f1o 6048  df-fv 6049  df-isom 6050  df-riota 6766  df-ov 6808  df-oprab 6809  df-mpt2 6810  df-of 7054  df-om 7223  df-1st 7325  df-2nd 7326  df-supp 7456  df-wrecs 7568  df-recs 7629  df-rdg 7667  df-1o 7721  df-2o 7722  df-oadd 7725  df-er 7903  df-map 8017  df-pm 8018  df-ixp 8067  df-en 8114  df-dom 8115  df-sdom 8116  df-fin 8117  df-fsupp 8433  df-fi 8474  df-sup 8505  df-inf 8506  df-oi 8572  df-card 8947  df-cda 9174  df-pnf 10260  df-mnf 10261  df-xr 10262  df-ltxr 10263  df-le 10264  df-sub 10452  df-neg 10453  df-div 10869  df-nn 11205  df-2 11263  df-3 11264  df-4 11265  df-5 11266  df-6 11267  df-7 11268  df-8 11269  df-9 11270  df-n0 11477  df-z 11562  df-dec 11678  df-uz 11872  df-q 11974  df-rp 12018  df-xneg 12131  df-xadd 12132  df-xmul 12133  df-ioo 12364  df-ioc 12365  df-ico 12366  df-icc 12367  df-fz 12512  df-fzo 12652  df-fl 12779  df-mod 12855  df-seq 12988  df-exp 13047  df-fac 13247  df-bc 13276  df-hash 13304  df-shft 13998  df-cj 14030  df-re 14031  df-im 14032  df-sqrt 14166  df-abs 14167  df-limsup 14393  df-clim 14410  df-rlim 14411  df-sum 14608  df-ef 14989  df-sin 14991  df-cos 14992  df-pi 14994  df-struct 16053  df-ndx 16054  df-slot 16055  df-base 16057  df-sets 16058  df-ress 16059  df-plusg 16148  df-mulr 16149  df-starv 16150  df-sca 16151  df-vsca 16152  df-ip 16153  df-tset 16154  df-ple 16155  df-ds 16158  df-unif 16159  df-hom 16160  df-cco 16161  df-rest 16277  df-topn 16278  df-0g 16296  df-gsum 16297  df-topgen 16298  df-pt 16299  df-prds 16302  df-xrs 16356  df-qtop 16361  df-imas 16362  df-xps 16364  df-mre 16440  df-mrc 16441  df-acs 16443  df-mgm 17435  df-sgrp 17477  df-mnd 17488  df-submnd 17529  df-mulg 17734  df-cntz 17942  df-cmn 18387  df-psmet 19932  df-xmet 19933  df-met 19934  df-bl 19935  df-mopn 19936  df-fbas 19937  df-fg 19938  df-cnfld 19941  df-top 20893  df-topon 20910  df-topsp 20931  df-bases 20944  df-cld 21017  df-ntr 21018  df-cls 21019  df-nei 21096  df-lp 21134  df-perf 21135  df-cn 21225  df-cnp 21226  df-haus 21313  df-tx 21559  df-hmeo 21752  df-fil 21843  df-fm 21935  df-flim 21936  df-flf 21937  df-xms 22318  df-ms 22319  df-tms 22320  df-cncf 22874  df-0p 23628  df-limc 23821  df-dv 23822  df-ply 24135  df-idp 24136  df-coe 24137  df-dgr 24138  df-log 24494  df-cxp 24495
This theorem is referenced by:  fta  24997
  Copyright terms: Public domain W3C validator