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

Theorem fta1lem 23780
Description: Lemma for fta1 23781. (Contributed by Mario Carneiro, 26-Jul-2014.)
Hypotheses
Ref Expression
fta1.1 𝑅 = (𝐹 “ {0})
fta1.2 (𝜑𝐷 ∈ ℕ0)
fta1.3 (𝜑𝐹 ∈ ((Poly‘ℂ) ∖ {0𝑝}))
fta1.4 (𝜑 → (deg‘𝐹) = (𝐷 + 1))
fta1.5 (𝜑𝐴 ∈ (𝐹 “ {0}))
fta1.6 (𝜑 → ∀𝑔 ∈ ((Poly‘ℂ) ∖ {0𝑝})((deg‘𝑔) = 𝐷 → ((𝑔 “ {0}) ∈ Fin ∧ (#‘(𝑔 “ {0})) ≤ (deg‘𝑔))))
Assertion
Ref Expression
fta1lem (𝜑 → (𝑅 ∈ Fin ∧ (#‘𝑅) ≤ (deg‘𝐹)))
Distinct variable groups:   𝐴,𝑔   𝐷,𝑔   𝑔,𝐹
Allowed substitution hints:   𝜑(𝑔)   𝑅(𝑔)

Proof of Theorem fta1lem
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 fta1.3 . . . . . . . . . 10 (𝜑𝐹 ∈ ((Poly‘ℂ) ∖ {0𝑝}))
2 eldifsn 4256 . . . . . . . . . 10 (𝐹 ∈ ((Poly‘ℂ) ∖ {0𝑝}) ↔ (𝐹 ∈ (Poly‘ℂ) ∧ 𝐹 ≠ 0𝑝))
31, 2sylib 206 . . . . . . . . 9 (𝜑 → (𝐹 ∈ (Poly‘ℂ) ∧ 𝐹 ≠ 0𝑝))
43simpld 473 . . . . . . . 8 (𝜑𝐹 ∈ (Poly‘ℂ))
5 fta1.5 . . . . . . . . . 10 (𝜑𝐴 ∈ (𝐹 “ {0}))
6 plyf 23672 . . . . . . . . . . 11 (𝐹 ∈ (Poly‘ℂ) → 𝐹:ℂ⟶ℂ)
7 ffn 5941 . . . . . . . . . . 11 (𝐹:ℂ⟶ℂ → 𝐹 Fn ℂ)
8 fniniseg 6228 . . . . . . . . . . 11 (𝐹 Fn ℂ → (𝐴 ∈ (𝐹 “ {0}) ↔ (𝐴 ∈ ℂ ∧ (𝐹𝐴) = 0)))
94, 6, 7, 84syl 19 . . . . . . . . . 10 (𝜑 → (𝐴 ∈ (𝐹 “ {0}) ↔ (𝐴 ∈ ℂ ∧ (𝐹𝐴) = 0)))
105, 9mpbid 220 . . . . . . . . 9 (𝜑 → (𝐴 ∈ ℂ ∧ (𝐹𝐴) = 0))
1110simpld 473 . . . . . . . 8 (𝜑𝐴 ∈ ℂ)
1210simprd 477 . . . . . . . 8 (𝜑 → (𝐹𝐴) = 0)
13 eqid 2606 . . . . . . . . 9 (Xp𝑓 − (ℂ × {𝐴})) = (Xp𝑓 − (ℂ × {𝐴}))
1413facth 23779 . . . . . . . 8 ((𝐹 ∈ (Poly‘ℂ) ∧ 𝐴 ∈ ℂ ∧ (𝐹𝐴) = 0) → 𝐹 = ((Xp𝑓 − (ℂ × {𝐴})) ∘𝑓 · (𝐹 quot (Xp𝑓 − (ℂ × {𝐴})))))
154, 11, 12, 14syl3anc 1317 . . . . . . 7 (𝜑𝐹 = ((Xp𝑓 − (ℂ × {𝐴})) ∘𝑓 · (𝐹 quot (Xp𝑓 − (ℂ × {𝐴})))))
1615cnveqd 5205 . . . . . 6 (𝜑𝐹 = ((Xp𝑓 − (ℂ × {𝐴})) ∘𝑓 · (𝐹 quot (Xp𝑓 − (ℂ × {𝐴})))))
1716imaeq1d 5368 . . . . 5 (𝜑 → (𝐹 “ {0}) = (((Xp𝑓 − (ℂ × {𝐴})) ∘𝑓 · (𝐹 quot (Xp𝑓 − (ℂ × {𝐴})))) “ {0}))
18 cnex 9870 . . . . . . 7 ℂ ∈ V
1918a1i 11 . . . . . 6 (𝜑 → ℂ ∈ V)
20 ssid 3583 . . . . . . . . 9 ℂ ⊆ ℂ
21 ax-1cn 9847 . . . . . . . . 9 1 ∈ ℂ
22 plyid 23683 . . . . . . . . 9 ((ℂ ⊆ ℂ ∧ 1 ∈ ℂ) → Xp ∈ (Poly‘ℂ))
2320, 21, 22mp2an 703 . . . . . . . 8 Xp ∈ (Poly‘ℂ)
24 plyconst 23680 . . . . . . . . 9 ((ℂ ⊆ ℂ ∧ 𝐴 ∈ ℂ) → (ℂ × {𝐴}) ∈ (Poly‘ℂ))
2520, 11, 24sylancr 693 . . . . . . . 8 (𝜑 → (ℂ × {𝐴}) ∈ (Poly‘ℂ))
26 plysubcl 23696 . . . . . . . 8 ((Xp ∈ (Poly‘ℂ) ∧ (ℂ × {𝐴}) ∈ (Poly‘ℂ)) → (Xp𝑓 − (ℂ × {𝐴})) ∈ (Poly‘ℂ))
2723, 25, 26sylancr 693 . . . . . . 7 (𝜑 → (Xp𝑓 − (ℂ × {𝐴})) ∈ (Poly‘ℂ))
28 plyf 23672 . . . . . . 7 ((Xp𝑓 − (ℂ × {𝐴})) ∈ (Poly‘ℂ) → (Xp𝑓 − (ℂ × {𝐴})):ℂ⟶ℂ)
2927, 28syl 17 . . . . . 6 (𝜑 → (Xp𝑓 − (ℂ × {𝐴})):ℂ⟶ℂ)
3013plyremlem 23777 . . . . . . . . . . . 12 (𝐴 ∈ ℂ → ((Xp𝑓 − (ℂ × {𝐴})) ∈ (Poly‘ℂ) ∧ (deg‘(Xp𝑓 − (ℂ × {𝐴}))) = 1 ∧ ((Xp𝑓 − (ℂ × {𝐴})) “ {0}) = {𝐴}))
3111, 30syl 17 . . . . . . . . . . 11 (𝜑 → ((Xp𝑓 − (ℂ × {𝐴})) ∈ (Poly‘ℂ) ∧ (deg‘(Xp𝑓 − (ℂ × {𝐴}))) = 1 ∧ ((Xp𝑓 − (ℂ × {𝐴})) “ {0}) = {𝐴}))
3231simp2d 1066 . . . . . . . . . 10 (𝜑 → (deg‘(Xp𝑓 − (ℂ × {𝐴}))) = 1)
33 ax-1ne0 9858 . . . . . . . . . . 11 1 ≠ 0
3433a1i 11 . . . . . . . . . 10 (𝜑 → 1 ≠ 0)
3532, 34eqnetrd 2845 . . . . . . . . 9 (𝜑 → (deg‘(Xp𝑓 − (ℂ × {𝐴}))) ≠ 0)
36 fveq2 6085 . . . . . . . . . . 11 ((Xp𝑓 − (ℂ × {𝐴})) = 0𝑝 → (deg‘(Xp𝑓 − (ℂ × {𝐴}))) = (deg‘0𝑝))
37 dgr0 23736 . . . . . . . . . . 11 (deg‘0𝑝) = 0
3836, 37syl6eq 2656 . . . . . . . . . 10 ((Xp𝑓 − (ℂ × {𝐴})) = 0𝑝 → (deg‘(Xp𝑓 − (ℂ × {𝐴}))) = 0)
3938necon3i 2810 . . . . . . . . 9 ((deg‘(Xp𝑓 − (ℂ × {𝐴}))) ≠ 0 → (Xp𝑓 − (ℂ × {𝐴})) ≠ 0𝑝)
4035, 39syl 17 . . . . . . . 8 (𝜑 → (Xp𝑓 − (ℂ × {𝐴})) ≠ 0𝑝)
41 quotcl2 23775 . . . . . . . 8 ((𝐹 ∈ (Poly‘ℂ) ∧ (Xp𝑓 − (ℂ × {𝐴})) ∈ (Poly‘ℂ) ∧ (Xp𝑓 − (ℂ × {𝐴})) ≠ 0𝑝) → (𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) ∈ (Poly‘ℂ))
424, 27, 40, 41syl3anc 1317 . . . . . . 7 (𝜑 → (𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) ∈ (Poly‘ℂ))
43 plyf 23672 . . . . . . 7 ((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) ∈ (Poly‘ℂ) → (𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))):ℂ⟶ℂ)
4442, 43syl 17 . . . . . 6 (𝜑 → (𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))):ℂ⟶ℂ)
45 ofmulrt 23755 . . . . . 6 ((ℂ ∈ V ∧ (Xp𝑓 − (ℂ × {𝐴})):ℂ⟶ℂ ∧ (𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))):ℂ⟶ℂ) → (((Xp𝑓 − (ℂ × {𝐴})) ∘𝑓 · (𝐹 quot (Xp𝑓 − (ℂ × {𝐴})))) “ {0}) = (((Xp𝑓 − (ℂ × {𝐴})) “ {0}) ∪ ((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0})))
4619, 29, 44, 45syl3anc 1317 . . . . 5 (𝜑 → (((Xp𝑓 − (ℂ × {𝐴})) ∘𝑓 · (𝐹 quot (Xp𝑓 − (ℂ × {𝐴})))) “ {0}) = (((Xp𝑓 − (ℂ × {𝐴})) “ {0}) ∪ ((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0})))
4731simp3d 1067 . . . . . 6 (𝜑 → ((Xp𝑓 − (ℂ × {𝐴})) “ {0}) = {𝐴})
4847uneq1d 3724 . . . . 5 (𝜑 → (((Xp𝑓 − (ℂ × {𝐴})) “ {0}) ∪ ((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0})) = ({𝐴} ∪ ((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0})))
4917, 46, 483eqtrd 2644 . . . 4 (𝜑 → (𝐹 “ {0}) = ({𝐴} ∪ ((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0})))
50 fta1.1 . . . 4 𝑅 = (𝐹 “ {0})
51 uncom 3715 . . . 4 (((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴}) = ({𝐴} ∪ ((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0}))
5249, 50, 513eqtr4g 2665 . . 3 (𝜑𝑅 = (((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴}))
533simprd 477 . . . . . . . . 9 (𝜑𝐹 ≠ 0𝑝)
5415eqcomd 2612 . . . . . . . . 9 (𝜑 → ((Xp𝑓 − (ℂ × {𝐴})) ∘𝑓 · (𝐹 quot (Xp𝑓 − (ℂ × {𝐴})))) = 𝐹)
55 0cnd 9886 . . . . . . . . . . 11 (𝜑 → 0 ∈ ℂ)
56 mul01 10063 . . . . . . . . . . . 12 (𝑥 ∈ ℂ → (𝑥 · 0) = 0)
5756adantl 480 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℂ) → (𝑥 · 0) = 0)
5819, 29, 55, 55, 57caofid1 6799 . . . . . . . . . 10 (𝜑 → ((Xp𝑓 − (ℂ × {𝐴})) ∘𝑓 · (ℂ × {0})) = (ℂ × {0}))
59 df-0p 23157 . . . . . . . . . . 11 0𝑝 = (ℂ × {0})
6059oveq2i 6535 . . . . . . . . . 10 ((Xp𝑓 − (ℂ × {𝐴})) ∘𝑓 · 0𝑝) = ((Xp𝑓 − (ℂ × {𝐴})) ∘𝑓 · (ℂ × {0}))
6158, 60, 593eqtr4g 2665 . . . . . . . . 9 (𝜑 → ((Xp𝑓 − (ℂ × {𝐴})) ∘𝑓 · 0𝑝) = 0𝑝)
6253, 54, 613netr4d 2855 . . . . . . . 8 (𝜑 → ((Xp𝑓 − (ℂ × {𝐴})) ∘𝑓 · (𝐹 quot (Xp𝑓 − (ℂ × {𝐴})))) ≠ ((Xp𝑓 − (ℂ × {𝐴})) ∘𝑓 · 0𝑝))
63 oveq2 6532 . . . . . . . . 9 ((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) = 0𝑝 → ((Xp𝑓 − (ℂ × {𝐴})) ∘𝑓 · (𝐹 quot (Xp𝑓 − (ℂ × {𝐴})))) = ((Xp𝑓 − (ℂ × {𝐴})) ∘𝑓 · 0𝑝))
6463necon3i 2810 . . . . . . . 8 (((Xp𝑓 − (ℂ × {𝐴})) ∘𝑓 · (𝐹 quot (Xp𝑓 − (ℂ × {𝐴})))) ≠ ((Xp𝑓 − (ℂ × {𝐴})) ∘𝑓 · 0𝑝) → (𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) ≠ 0𝑝)
6562, 64syl 17 . . . . . . 7 (𝜑 → (𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) ≠ 0𝑝)
66 eldifsn 4256 . . . . . . 7 ((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) ∈ ((Poly‘ℂ) ∖ {0𝑝}) ↔ ((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) ∈ (Poly‘ℂ) ∧ (𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) ≠ 0𝑝))
6742, 65, 66sylanbrc 694 . . . . . 6 (𝜑 → (𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) ∈ ((Poly‘ℂ) ∖ {0𝑝}))
68 fta1.6 . . . . . 6 (𝜑 → ∀𝑔 ∈ ((Poly‘ℂ) ∖ {0𝑝})((deg‘𝑔) = 𝐷 → ((𝑔 “ {0}) ∈ Fin ∧ (#‘(𝑔 “ {0})) ≤ (deg‘𝑔))))
6921a1i 11 . . . . . . 7 (𝜑 → 1 ∈ ℂ)
70 dgrcl 23707 . . . . . . . . 9 ((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) ∈ (Poly‘ℂ) → (deg‘(𝐹 quot (Xp𝑓 − (ℂ × {𝐴})))) ∈ ℕ0)
7142, 70syl 17 . . . . . . . 8 (𝜑 → (deg‘(𝐹 quot (Xp𝑓 − (ℂ × {𝐴})))) ∈ ℕ0)
7271nn0cnd 11197 . . . . . . 7 (𝜑 → (deg‘(𝐹 quot (Xp𝑓 − (ℂ × {𝐴})))) ∈ ℂ)
73 fta1.2 . . . . . . . 8 (𝜑𝐷 ∈ ℕ0)
7473nn0cnd 11197 . . . . . . 7 (𝜑𝐷 ∈ ℂ)
75 addcom 10070 . . . . . . . . 9 ((1 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (1 + 𝐷) = (𝐷 + 1))
7621, 74, 75sylancr 693 . . . . . . . 8 (𝜑 → (1 + 𝐷) = (𝐷 + 1))
7715fveq2d 6089 . . . . . . . . 9 (𝜑 → (deg‘𝐹) = (deg‘((Xp𝑓 − (ℂ × {𝐴})) ∘𝑓 · (𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))))))
78 fta1.4 . . . . . . . . 9 (𝜑 → (deg‘𝐹) = (𝐷 + 1))
79 eqid 2606 . . . . . . . . . . 11 (deg‘(Xp𝑓 − (ℂ × {𝐴}))) = (deg‘(Xp𝑓 − (ℂ × {𝐴})))
80 eqid 2606 . . . . . . . . . . 11 (deg‘(𝐹 quot (Xp𝑓 − (ℂ × {𝐴})))) = (deg‘(𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))))
8179, 80dgrmul 23744 . . . . . . . . . 10 ((((Xp𝑓 − (ℂ × {𝐴})) ∈ (Poly‘ℂ) ∧ (Xp𝑓 − (ℂ × {𝐴})) ≠ 0𝑝) ∧ ((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) ∈ (Poly‘ℂ) ∧ (𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) ≠ 0𝑝)) → (deg‘((Xp𝑓 − (ℂ × {𝐴})) ∘𝑓 · (𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))))) = ((deg‘(Xp𝑓 − (ℂ × {𝐴}))) + (deg‘(𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))))))
8227, 40, 42, 65, 81syl22anc 1318 . . . . . . . . 9 (𝜑 → (deg‘((Xp𝑓 − (ℂ × {𝐴})) ∘𝑓 · (𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))))) = ((deg‘(Xp𝑓 − (ℂ × {𝐴}))) + (deg‘(𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))))))
8377, 78, 823eqtr3d 2648 . . . . . . . 8 (𝜑 → (𝐷 + 1) = ((deg‘(Xp𝑓 − (ℂ × {𝐴}))) + (deg‘(𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))))))
8432oveq1d 6539 . . . . . . . 8 (𝜑 → ((deg‘(Xp𝑓 − (ℂ × {𝐴}))) + (deg‘(𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))))) = (1 + (deg‘(𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))))))
8576, 83, 843eqtrrd 2645 . . . . . . 7 (𝜑 → (1 + (deg‘(𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))))) = (1 + 𝐷))
8669, 72, 74, 85addcanad 10089 . . . . . 6 (𝜑 → (deg‘(𝐹 quot (Xp𝑓 − (ℂ × {𝐴})))) = 𝐷)
87 fveq2 6085 . . . . . . . . 9 (𝑔 = (𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) → (deg‘𝑔) = (deg‘(𝐹 quot (Xp𝑓 − (ℂ × {𝐴})))))
8887eqeq1d 2608 . . . . . . . 8 (𝑔 = (𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) → ((deg‘𝑔) = 𝐷 ↔ (deg‘(𝐹 quot (Xp𝑓 − (ℂ × {𝐴})))) = 𝐷))
89 cnveq 5203 . . . . . . . . . . 11 (𝑔 = (𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) → 𝑔 = (𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))))
9089imaeq1d 5368 . . . . . . . . . 10 (𝑔 = (𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) → (𝑔 “ {0}) = ((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0}))
9190eleq1d 2668 . . . . . . . . 9 (𝑔 = (𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) → ((𝑔 “ {0}) ∈ Fin ↔ ((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0}) ∈ Fin))
9290fveq2d 6089 . . . . . . . . . 10 (𝑔 = (𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) → (#‘(𝑔 “ {0})) = (#‘((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0})))
9392, 87breq12d 4587 . . . . . . . . 9 (𝑔 = (𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) → ((#‘(𝑔 “ {0})) ≤ (deg‘𝑔) ↔ (#‘((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0})) ≤ (deg‘(𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))))))
9491, 93anbi12d 742 . . . . . . . 8 (𝑔 = (𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) → (((𝑔 “ {0}) ∈ Fin ∧ (#‘(𝑔 “ {0})) ≤ (deg‘𝑔)) ↔ (((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0}) ∈ Fin ∧ (#‘((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0})) ≤ (deg‘(𝐹 quot (Xp𝑓 − (ℂ × {𝐴})))))))
9588, 94imbi12d 332 . . . . . . 7 (𝑔 = (𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) → (((deg‘𝑔) = 𝐷 → ((𝑔 “ {0}) ∈ Fin ∧ (#‘(𝑔 “ {0})) ≤ (deg‘𝑔))) ↔ ((deg‘(𝐹 quot (Xp𝑓 − (ℂ × {𝐴})))) = 𝐷 → (((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0}) ∈ Fin ∧ (#‘((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0})) ≤ (deg‘(𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))))))))
9695rspcv 3274 . . . . . 6 ((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) ∈ ((Poly‘ℂ) ∖ {0𝑝}) → (∀𝑔 ∈ ((Poly‘ℂ) ∖ {0𝑝})((deg‘𝑔) = 𝐷 → ((𝑔 “ {0}) ∈ Fin ∧ (#‘(𝑔 “ {0})) ≤ (deg‘𝑔))) → ((deg‘(𝐹 quot (Xp𝑓 − (ℂ × {𝐴})))) = 𝐷 → (((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0}) ∈ Fin ∧ (#‘((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0})) ≤ (deg‘(𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))))))))
9767, 68, 86, 96syl3c 63 . . . . 5 (𝜑 → (((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0}) ∈ Fin ∧ (#‘((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0})) ≤ (deg‘(𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))))))
9897simpld 473 . . . 4 (𝜑 → ((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0}) ∈ Fin)
99 snfi 7897 . . . 4 {𝐴} ∈ Fin
100 unfi 8086 . . . 4 ((((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0}) ∈ Fin ∧ {𝐴} ∈ Fin) → (((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴}) ∈ Fin)
10198, 99, 100sylancl 692 . . 3 (𝜑 → (((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴}) ∈ Fin)
10252, 101eqeltrd 2684 . 2 (𝜑𝑅 ∈ Fin)
10352fveq2d 6089 . . 3 (𝜑 → (#‘𝑅) = (#‘(((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴})))
104 hashcl 12958 . . . . . 6 ((((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴}) ∈ Fin → (#‘(((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴})) ∈ ℕ0)
105101, 104syl 17 . . . . 5 (𝜑 → (#‘(((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴})) ∈ ℕ0)
106105nn0red 11196 . . . 4 (𝜑 → (#‘(((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴})) ∈ ℝ)
107 hashcl 12958 . . . . . . 7 (((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0}) ∈ Fin → (#‘((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0})) ∈ ℕ0)
10898, 107syl 17 . . . . . 6 (𝜑 → (#‘((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0})) ∈ ℕ0)
109108nn0red 11196 . . . . 5 (𝜑 → (#‘((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0})) ∈ ℝ)
110 peano2re 10057 . . . . 5 ((#‘((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0})) ∈ ℝ → ((#‘((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0})) + 1) ∈ ℝ)
111109, 110syl 17 . . . 4 (𝜑 → ((#‘((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0})) + 1) ∈ ℝ)
112 dgrcl 23707 . . . . . 6 (𝐹 ∈ (Poly‘ℂ) → (deg‘𝐹) ∈ ℕ0)
1134, 112syl 17 . . . . 5 (𝜑 → (deg‘𝐹) ∈ ℕ0)
114113nn0red 11196 . . . 4 (𝜑 → (deg‘𝐹) ∈ ℝ)
115 hashun2 12982 . . . . . 6 ((((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0}) ∈ Fin ∧ {𝐴} ∈ Fin) → (#‘(((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴})) ≤ ((#‘((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0})) + (#‘{𝐴})))
11698, 99, 115sylancl 692 . . . . 5 (𝜑 → (#‘(((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴})) ≤ ((#‘((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0})) + (#‘{𝐴})))
117 hashsng 12969 . . . . . . 7 (𝐴 ∈ ℂ → (#‘{𝐴}) = 1)
11811, 117syl 17 . . . . . 6 (𝜑 → (#‘{𝐴}) = 1)
119118oveq2d 6540 . . . . 5 (𝜑 → ((#‘((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0})) + (#‘{𝐴})) = ((#‘((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0})) + 1))
120116, 119breqtrd 4600 . . . 4 (𝜑 → (#‘(((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴})) ≤ ((#‘((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0})) + 1))
12173nn0red 11196 . . . . . 6 (𝜑𝐷 ∈ ℝ)
122 1red 9908 . . . . . 6 (𝜑 → 1 ∈ ℝ)
12397simprd 477 . . . . . . 7 (𝜑 → (#‘((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0})) ≤ (deg‘(𝐹 quot (Xp𝑓 − (ℂ × {𝐴})))))
124123, 86breqtrd 4600 . . . . . 6 (𝜑 → (#‘((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0})) ≤ 𝐷)
125109, 121, 122, 124leadd1dd 10487 . . . . 5 (𝜑 → ((#‘((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0})) + 1) ≤ (𝐷 + 1))
126125, 78breqtrrd 4602 . . . 4 (𝜑 → ((#‘((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0})) + 1) ≤ (deg‘𝐹))
127106, 111, 114, 120, 126letrd 10042 . . 3 (𝜑 → (#‘(((𝐹 quot (Xp𝑓 − (ℂ × {𝐴}))) “ {0}) ∪ {𝐴})) ≤ (deg‘𝐹))
128103, 127eqbrtrd 4596 . 2 (𝜑 → (#‘𝑅) ≤ (deg‘𝐹))
129102, 128jca 552 1 (𝜑 → (𝑅 ∈ Fin ∧ (#‘𝑅) ≤ (deg‘𝐹)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1976  wne 2776  wral 2892  Vcvv 3169  cdif 3533  cun 3534  wss 3536  {csn 4121   class class class wbr 4574   × cxp 5023  ccnv 5024  cima 5028   Fn wfn 5782  wf 5783  cfv 5787  (class class class)co 6524  𝑓 cof 6767  Fincfn 7815  cc 9787  cr 9788  0cc0 9789  1c1 9790   + caddc 9792   · cmul 9794  cle 9928  cmin 10114  0cn0 11136  #chash 12931  0𝑝c0p 23156  Polycply 23658  Xpcidp 23659  degcdgr 23661   quot cquot 23763
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-rep 4690  ax-sep 4700  ax-nul 4709  ax-pow 4761  ax-pr 4825  ax-un 6821  ax-inf2 8395  ax-cnex 9845  ax-resscn 9846  ax-1cn 9847  ax-icn 9848  ax-addcl 9849  ax-addrcl 9850  ax-mulcl 9851  ax-mulrcl 9852  ax-mulcom 9853  ax-addass 9854  ax-mulass 9855  ax-distr 9856  ax-i2m1 9857  ax-1ne0 9858  ax-1rid 9859  ax-rnegex 9860  ax-rrecex 9861  ax-cnre 9862  ax-pre-lttri 9863  ax-pre-lttrn 9864  ax-pre-ltadd 9865  ax-pre-mulgt0 9866  ax-pre-sup 9867  ax-addf 9868
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-nel 2779  df-ral 2897  df-rex 2898  df-reu 2899  df-rmo 2900  df-rab 2901  df-v 3171  df-sbc 3399  df-csb 3496  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-pss 3552  df-nul 3871  df-if 4033  df-pw 4106  df-sn 4122  df-pr 4124  df-tp 4126  df-op 4128  df-uni 4364  df-int 4402  df-iun 4448  df-br 4575  df-opab 4635  df-mpt 4636  df-tr 4672  df-eprel 4936  df-id 4940  df-po 4946  df-so 4947  df-fr 4984  df-se 4985  df-we 4986  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038  df-pred 5580  df-ord 5626  df-on 5627  df-lim 5628  df-suc 5629  df-iota 5751  df-fun 5789  df-fn 5790  df-f 5791  df-f1 5792  df-fo 5793  df-f1o 5794  df-fv 5795  df-isom 5796  df-riota 6486  df-ov 6527  df-oprab 6528  df-mpt2 6529  df-of 6769  df-om 6932  df-1st 7033  df-2nd 7034  df-wrecs 7268  df-recs 7329  df-rdg 7367  df-1o 7421  df-oadd 7425  df-er 7603  df-map 7720  df-pm 7721  df-en 7816  df-dom 7817  df-sdom 7818  df-fin 7819  df-sup 8205  df-inf 8206  df-oi 8272  df-card 8622  df-cda 8847  df-pnf 9929  df-mnf 9930  df-xr 9931  df-ltxr 9932  df-le 9933  df-sub 10116  df-neg 10117  df-div 10531  df-nn 10865  df-2 10923  df-3 10924  df-n0 11137  df-z 11208  df-uz 11517  df-rp 11662  df-fz 12150  df-fzo 12287  df-fl 12407  df-seq 12616  df-exp 12675  df-hash 12932  df-cj 13630  df-re 13631  df-im 13632  df-sqrt 13766  df-abs 13767  df-clim 14010  df-rlim 14011  df-sum 14208  df-0p 23157  df-ply 23662  df-idp 23663  df-coe 23664  df-dgr 23665  df-quot 23764
This theorem is referenced by:  fta1  23781
  Copyright terms: Public domain W3C validator