Metamath Proof Explorer


Theorem fta1lem

Description: Lemma for fta1 . (Contributed by Mario Carneiro, 26-Jul-2014)

Ref Expression
Hypotheses 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 fta1lem ( 𝜑 → ( 𝑅 ∈ Fin ∧ ( ♯ ‘ 𝑅 ) ≤ ( deg ‘ 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 fta1.1 𝑅 = ( 𝐹 “ { 0 } )
2 fta1.2 ( 𝜑𝐷 ∈ ℕ0 )
3 fta1.3 ( 𝜑𝐹 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) )
4 fta1.4 ( 𝜑 → ( deg ‘ 𝐹 ) = ( 𝐷 + 1 ) )
5 fta1.5 ( 𝜑𝐴 ∈ ( 𝐹 “ { 0 } ) )
6 fta1.6 ( 𝜑 → ∀ 𝑔 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑔 ) = 𝐷 → ( ( 𝑔 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑔 “ { 0 } ) ) ≤ ( deg ‘ 𝑔 ) ) ) )
7 eldifsn ( 𝐹 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ↔ ( 𝐹 ∈ ( Poly ‘ ℂ ) ∧ 𝐹 ≠ 0𝑝 ) )
8 3 7 sylib ( 𝜑 → ( 𝐹 ∈ ( Poly ‘ ℂ ) ∧ 𝐹 ≠ 0𝑝 ) )
9 8 simpld ( 𝜑𝐹 ∈ ( Poly ‘ ℂ ) )
10 plyf ( 𝐹 ∈ ( Poly ‘ ℂ ) → 𝐹 : ℂ ⟶ ℂ )
11 ffn ( 𝐹 : ℂ ⟶ ℂ → 𝐹 Fn ℂ )
12 fniniseg ( 𝐹 Fn ℂ → ( 𝐴 ∈ ( 𝐹 “ { 0 } ) ↔ ( 𝐴 ∈ ℂ ∧ ( 𝐹𝐴 ) = 0 ) ) )
13 9 10 11 12 4syl ( 𝜑 → ( 𝐴 ∈ ( 𝐹 “ { 0 } ) ↔ ( 𝐴 ∈ ℂ ∧ ( 𝐹𝐴 ) = 0 ) ) )
14 5 13 mpbid ( 𝜑 → ( 𝐴 ∈ ℂ ∧ ( 𝐹𝐴 ) = 0 ) )
15 14 simpld ( 𝜑𝐴 ∈ ℂ )
16 14 simprd ( 𝜑 → ( 𝐹𝐴 ) = 0 )
17 eqid ( Xpf − ( ℂ × { 𝐴 } ) ) = ( Xpf − ( ℂ × { 𝐴 } ) )
18 17 facth ( ( 𝐹 ∈ ( Poly ‘ ℂ ) ∧ 𝐴 ∈ ℂ ∧ ( 𝐹𝐴 ) = 0 ) → 𝐹 = ( ( Xpf − ( ℂ × { 𝐴 } ) ) ∘f · ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ) )
19 9 15 16 18 syl3anc ( 𝜑𝐹 = ( ( Xpf − ( ℂ × { 𝐴 } ) ) ∘f · ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ) )
20 19 cnveqd ( 𝜑 𝐹 = ( ( Xpf − ( ℂ × { 𝐴 } ) ) ∘f · ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ) )
21 20 imaeq1d ( 𝜑 → ( 𝐹 “ { 0 } ) = ( ( ( Xpf − ( ℂ × { 𝐴 } ) ) ∘f · ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ) “ { 0 } ) )
22 cnex ℂ ∈ V
23 22 a1i ( 𝜑 → ℂ ∈ V )
24 ssid ℂ ⊆ ℂ
25 ax-1cn 1 ∈ ℂ
26 plyid ( ( ℂ ⊆ ℂ ∧ 1 ∈ ℂ ) → Xp ∈ ( Poly ‘ ℂ ) )
27 24 25 26 mp2an Xp ∈ ( Poly ‘ ℂ )
28 plyconst ( ( ℂ ⊆ ℂ ∧ 𝐴 ∈ ℂ ) → ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ ℂ ) )
29 24 15 28 sylancr ( 𝜑 → ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ ℂ ) )
30 plysubcl ( ( Xp ∈ ( Poly ‘ ℂ ) ∧ ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ ℂ ) ) → ( Xpf − ( ℂ × { 𝐴 } ) ) ∈ ( Poly ‘ ℂ ) )
31 27 29 30 sylancr ( 𝜑 → ( Xpf − ( ℂ × { 𝐴 } ) ) ∈ ( Poly ‘ ℂ ) )
32 plyf ( ( Xpf − ( ℂ × { 𝐴 } ) ) ∈ ( Poly ‘ ℂ ) → ( Xpf − ( ℂ × { 𝐴 } ) ) : ℂ ⟶ ℂ )
33 31 32 syl ( 𝜑 → ( Xpf − ( ℂ × { 𝐴 } ) ) : ℂ ⟶ ℂ )
34 17 plyremlem ( 𝐴 ∈ ℂ → ( ( Xpf − ( ℂ × { 𝐴 } ) ) ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ ( Xpf − ( ℂ × { 𝐴 } ) ) ) = 1 ∧ ( ( Xpf − ( ℂ × { 𝐴 } ) ) “ { 0 } ) = { 𝐴 } ) )
35 15 34 syl ( 𝜑 → ( ( Xpf − ( ℂ × { 𝐴 } ) ) ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ ( Xpf − ( ℂ × { 𝐴 } ) ) ) = 1 ∧ ( ( Xpf − ( ℂ × { 𝐴 } ) ) “ { 0 } ) = { 𝐴 } ) )
36 35 simp2d ( 𝜑 → ( deg ‘ ( Xpf − ( ℂ × { 𝐴 } ) ) ) = 1 )
37 ax-1ne0 1 ≠ 0
38 37 a1i ( 𝜑 → 1 ≠ 0 )
39 36 38 eqnetrd ( 𝜑 → ( deg ‘ ( Xpf − ( ℂ × { 𝐴 } ) ) ) ≠ 0 )
40 fveq2 ( ( Xpf − ( ℂ × { 𝐴 } ) ) = 0𝑝 → ( deg ‘ ( Xpf − ( ℂ × { 𝐴 } ) ) ) = ( deg ‘ 0𝑝 ) )
41 dgr0 ( deg ‘ 0𝑝 ) = 0
42 40 41 eqtrdi ( ( Xpf − ( ℂ × { 𝐴 } ) ) = 0𝑝 → ( deg ‘ ( Xpf − ( ℂ × { 𝐴 } ) ) ) = 0 )
43 42 necon3i ( ( deg ‘ ( Xpf − ( ℂ × { 𝐴 } ) ) ) ≠ 0 → ( Xpf − ( ℂ × { 𝐴 } ) ) ≠ 0𝑝 )
44 39 43 syl ( 𝜑 → ( Xpf − ( ℂ × { 𝐴 } ) ) ≠ 0𝑝 )
45 quotcl2 ( ( 𝐹 ∈ ( Poly ‘ ℂ ) ∧ ( Xpf − ( ℂ × { 𝐴 } ) ) ∈ ( Poly ‘ ℂ ) ∧ ( Xpf − ( ℂ × { 𝐴 } ) ) ≠ 0𝑝 ) → ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ∈ ( Poly ‘ ℂ ) )
46 9 31 44 45 syl3anc ( 𝜑 → ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ∈ ( Poly ‘ ℂ ) )
47 plyf ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ∈ ( Poly ‘ ℂ ) → ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) : ℂ ⟶ ℂ )
48 46 47 syl ( 𝜑 → ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) : ℂ ⟶ ℂ )
49 ofmulrt ( ( ℂ ∈ V ∧ ( Xpf − ( ℂ × { 𝐴 } ) ) : ℂ ⟶ ℂ ∧ ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) : ℂ ⟶ ℂ ) → ( ( ( Xpf − ( ℂ × { 𝐴 } ) ) ∘f · ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ) “ { 0 } ) = ( ( ( Xpf − ( ℂ × { 𝐴 } ) ) “ { 0 } ) ∪ ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) )
50 23 33 48 49 syl3anc ( 𝜑 → ( ( ( Xpf − ( ℂ × { 𝐴 } ) ) ∘f · ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ) “ { 0 } ) = ( ( ( Xpf − ( ℂ × { 𝐴 } ) ) “ { 0 } ) ∪ ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) )
51 35 simp3d ( 𝜑 → ( ( Xpf − ( ℂ × { 𝐴 } ) ) “ { 0 } ) = { 𝐴 } )
52 51 uneq1d ( 𝜑 → ( ( ( Xpf − ( ℂ × { 𝐴 } ) ) “ { 0 } ) ∪ ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) = ( { 𝐴 } ∪ ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) )
53 21 50 52 3eqtrd ( 𝜑 → ( 𝐹 “ { 0 } ) = ( { 𝐴 } ∪ ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) )
54 uncom ( ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∪ { 𝐴 } ) = ( { 𝐴 } ∪ ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) )
55 53 1 54 3eqtr4g ( 𝜑𝑅 = ( ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∪ { 𝐴 } ) )
56 25 a1i ( 𝜑 → 1 ∈ ℂ )
57 dgrcl ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ∈ ( Poly ‘ ℂ ) → ( deg ‘ ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ) ∈ ℕ0 )
58 46 57 syl ( 𝜑 → ( deg ‘ ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ) ∈ ℕ0 )
59 58 nn0cnd ( 𝜑 → ( deg ‘ ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ) ∈ ℂ )
60 2 nn0cnd ( 𝜑𝐷 ∈ ℂ )
61 addcom ( ( 1 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( 1 + 𝐷 ) = ( 𝐷 + 1 ) )
62 25 60 61 sylancr ( 𝜑 → ( 1 + 𝐷 ) = ( 𝐷 + 1 ) )
63 19 fveq2d ( 𝜑 → ( deg ‘ 𝐹 ) = ( deg ‘ ( ( Xpf − ( ℂ × { 𝐴 } ) ) ∘f · ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ) ) )
64 8 simprd ( 𝜑𝐹 ≠ 0𝑝 )
65 19 eqcomd ( 𝜑 → ( ( Xpf − ( ℂ × { 𝐴 } ) ) ∘f · ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ) = 𝐹 )
66 0cnd ( 𝜑 → 0 ∈ ℂ )
67 mul01 ( 𝑥 ∈ ℂ → ( 𝑥 · 0 ) = 0 )
68 67 adantl ( ( 𝜑𝑥 ∈ ℂ ) → ( 𝑥 · 0 ) = 0 )
69 23 33 66 66 68 caofid1 ( 𝜑 → ( ( Xpf − ( ℂ × { 𝐴 } ) ) ∘f · ( ℂ × { 0 } ) ) = ( ℂ × { 0 } ) )
70 df-0p 0𝑝 = ( ℂ × { 0 } )
71 70 oveq2i ( ( Xpf − ( ℂ × { 𝐴 } ) ) ∘f · 0𝑝 ) = ( ( Xpf − ( ℂ × { 𝐴 } ) ) ∘f · ( ℂ × { 0 } ) )
72 69 71 70 3eqtr4g ( 𝜑 → ( ( Xpf − ( ℂ × { 𝐴 } ) ) ∘f · 0𝑝 ) = 0𝑝 )
73 64 65 72 3netr4d ( 𝜑 → ( ( Xpf − ( ℂ × { 𝐴 } ) ) ∘f · ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ) ≠ ( ( Xpf − ( ℂ × { 𝐴 } ) ) ∘f · 0𝑝 ) )
74 oveq2 ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) = 0𝑝 → ( ( Xpf − ( ℂ × { 𝐴 } ) ) ∘f · ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ) = ( ( Xpf − ( ℂ × { 𝐴 } ) ) ∘f · 0𝑝 ) )
75 74 necon3i ( ( ( Xpf − ( ℂ × { 𝐴 } ) ) ∘f · ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ) ≠ ( ( Xpf − ( ℂ × { 𝐴 } ) ) ∘f · 0𝑝 ) → ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ≠ 0𝑝 )
76 73 75 syl ( 𝜑 → ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ≠ 0𝑝 )
77 eqid ( deg ‘ ( Xpf − ( ℂ × { 𝐴 } ) ) ) = ( deg ‘ ( Xpf − ( ℂ × { 𝐴 } ) ) )
78 eqid ( deg ‘ ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ) = ( deg ‘ ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) )
79 77 78 dgrmul ( ( ( ( Xpf − ( ℂ × { 𝐴 } ) ) ∈ ( Poly ‘ ℂ ) ∧ ( Xpf − ( ℂ × { 𝐴 } ) ) ≠ 0𝑝 ) ∧ ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ∈ ( Poly ‘ ℂ ) ∧ ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ≠ 0𝑝 ) ) → ( deg ‘ ( ( Xpf − ( ℂ × { 𝐴 } ) ) ∘f · ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ) ) = ( ( deg ‘ ( Xpf − ( ℂ × { 𝐴 } ) ) ) + ( deg ‘ ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ) ) )
80 31 44 46 76 79 syl22anc ( 𝜑 → ( deg ‘ ( ( Xpf − ( ℂ × { 𝐴 } ) ) ∘f · ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ) ) = ( ( deg ‘ ( Xpf − ( ℂ × { 𝐴 } ) ) ) + ( deg ‘ ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ) ) )
81 63 4 80 3eqtr3d ( 𝜑 → ( 𝐷 + 1 ) = ( ( deg ‘ ( Xpf − ( ℂ × { 𝐴 } ) ) ) + ( deg ‘ ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ) ) )
82 36 oveq1d ( 𝜑 → ( ( deg ‘ ( Xpf − ( ℂ × { 𝐴 } ) ) ) + ( deg ‘ ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ) ) = ( 1 + ( deg ‘ ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ) ) )
83 62 81 82 3eqtrrd ( 𝜑 → ( 1 + ( deg ‘ ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ) ) = ( 1 + 𝐷 ) )
84 56 59 60 83 addcanad ( 𝜑 → ( deg ‘ ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ) = 𝐷 )
85 fveqeq2 ( 𝑔 = ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) → ( ( deg ‘ 𝑔 ) = 𝐷 ↔ ( deg ‘ ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ) = 𝐷 ) )
86 cnveq ( 𝑔 = ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) → 𝑔 = ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) )
87 86 imaeq1d ( 𝑔 = ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) → ( 𝑔 “ { 0 } ) = ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) )
88 87 eleq1d ( 𝑔 = ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) → ( ( 𝑔 “ { 0 } ) ∈ Fin ↔ ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∈ Fin ) )
89 87 fveq2d ( 𝑔 = ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) → ( ♯ ‘ ( 𝑔 “ { 0 } ) ) = ( ♯ ‘ ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) )
90 fveq2 ( 𝑔 = ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) → ( deg ‘ 𝑔 ) = ( deg ‘ ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ) )
91 89 90 breq12d ( 𝑔 = ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) → ( ( ♯ ‘ ( 𝑔 “ { 0 } ) ) ≤ ( deg ‘ 𝑔 ) ↔ ( ♯ ‘ ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) ≤ ( deg ‘ ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ) ) )
92 88 91 anbi12d ( 𝑔 = ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) → ( ( ( 𝑔 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑔 “ { 0 } ) ) ≤ ( deg ‘ 𝑔 ) ) ↔ ( ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) ≤ ( deg ‘ ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ) ) ) )
93 85 92 imbi12d ( 𝑔 = ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) → ( ( ( deg ‘ 𝑔 ) = 𝐷 → ( ( 𝑔 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( 𝑔 “ { 0 } ) ) ≤ ( deg ‘ 𝑔 ) ) ) ↔ ( ( deg ‘ ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ) = 𝐷 → ( ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) ≤ ( deg ‘ ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ) ) ) ) )
94 eldifsn ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ↔ ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ∈ ( Poly ‘ ℂ ) ∧ ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ≠ 0𝑝 ) )
95 46 76 94 sylanbrc ( 𝜑 → ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) )
96 93 6 95 rspcdva ( 𝜑 → ( ( deg ‘ ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ) = 𝐷 → ( ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) ≤ ( deg ‘ ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ) ) ) )
97 84 96 mpd ( 𝜑 → ( ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) ≤ ( deg ‘ ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ) ) )
98 97 simpld ( 𝜑 → ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∈ Fin )
99 snfi { 𝐴 } ∈ Fin
100 unfi ( ( ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∈ Fin ∧ { 𝐴 } ∈ Fin ) → ( ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∪ { 𝐴 } ) ∈ Fin )
101 98 99 100 sylancl ( 𝜑 → ( ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∪ { 𝐴 } ) ∈ Fin )
102 55 101 eqeltrd ( 𝜑𝑅 ∈ Fin )
103 55 fveq2d ( 𝜑 → ( ♯ ‘ 𝑅 ) = ( ♯ ‘ ( ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∪ { 𝐴 } ) ) )
104 hashcl ( ( ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∪ { 𝐴 } ) ∈ Fin → ( ♯ ‘ ( ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∪ { 𝐴 } ) ) ∈ ℕ0 )
105 101 104 syl ( 𝜑 → ( ♯ ‘ ( ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∪ { 𝐴 } ) ) ∈ ℕ0 )
106 105 nn0red ( 𝜑 → ( ♯ ‘ ( ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∪ { 𝐴 } ) ) ∈ ℝ )
107 hashcl ( ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∈ Fin → ( ♯ ‘ ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) ∈ ℕ0 )
108 98 107 syl ( 𝜑 → ( ♯ ‘ ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) ∈ ℕ0 )
109 108 nn0red ( 𝜑 → ( ♯ ‘ ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) ∈ ℝ )
110 peano2re ( ( ♯ ‘ ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) ∈ ℝ → ( ( ♯ ‘ ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) + 1 ) ∈ ℝ )
111 109 110 syl ( 𝜑 → ( ( ♯ ‘ ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) + 1 ) ∈ ℝ )
112 dgrcl ( 𝐹 ∈ ( Poly ‘ ℂ ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )
113 9 112 syl ( 𝜑 → ( deg ‘ 𝐹 ) ∈ ℕ0 )
114 113 nn0red ( 𝜑 → ( deg ‘ 𝐹 ) ∈ ℝ )
115 hashun2 ( ( ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∈ Fin ∧ { 𝐴 } ∈ Fin ) → ( ♯ ‘ ( ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∪ { 𝐴 } ) ) ≤ ( ( ♯ ‘ ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) + ( ♯ ‘ { 𝐴 } ) ) )
116 98 99 115 sylancl ( 𝜑 → ( ♯ ‘ ( ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∪ { 𝐴 } ) ) ≤ ( ( ♯ ‘ ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) + ( ♯ ‘ { 𝐴 } ) ) )
117 hashsng ( 𝐴 ∈ ℂ → ( ♯ ‘ { 𝐴 } ) = 1 )
118 15 117 syl ( 𝜑 → ( ♯ ‘ { 𝐴 } ) = 1 )
119 118 oveq2d ( 𝜑 → ( ( ♯ ‘ ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) + ( ♯ ‘ { 𝐴 } ) ) = ( ( ♯ ‘ ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) + 1 ) )
120 116 119 breqtrd ( 𝜑 → ( ♯ ‘ ( ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∪ { 𝐴 } ) ) ≤ ( ( ♯ ‘ ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) + 1 ) )
121 2 nn0red ( 𝜑𝐷 ∈ ℝ )
122 1red ( 𝜑 → 1 ∈ ℝ )
123 97 simprd ( 𝜑 → ( ♯ ‘ ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) ≤ ( deg ‘ ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) ) )
124 123 84 breqtrd ( 𝜑 → ( ♯ ‘ ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) ≤ 𝐷 )
125 109 121 122 124 leadd1dd ( 𝜑 → ( ( ♯ ‘ ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) + 1 ) ≤ ( 𝐷 + 1 ) )
126 125 4 breqtrrd ( 𝜑 → ( ( ♯ ‘ ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) + 1 ) ≤ ( deg ‘ 𝐹 ) )
127 106 111 114 120 126 letrd ( 𝜑 → ( ♯ ‘ ( ( ( 𝐹 quot ( Xpf − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∪ { 𝐴 } ) ) ≤ ( deg ‘ 𝐹 ) )
128 103 127 eqbrtrd ( 𝜑 → ( ♯ ‘ 𝑅 ) ≤ ( deg ‘ 𝐹 ) )
129 102 128 jca ( 𝜑 → ( 𝑅 ∈ Fin ∧ ( ♯ ‘ 𝑅 ) ≤ ( deg ‘ 𝐹 ) ) )