Metamath Proof Explorer


Theorem constrfin

Description: Each step of the construction of constructible numbers is finite. (Contributed by Thierry Arnoux, 6-Jul-2025)

Ref Expression
Hypotheses constr0.1 C = rec s V x | a s b s c s d s t r x = a + t b a x = c + r d c b a d c 0 a s b s c s e s f s t x = a + t b a x c = e f a s b s c s d s e s f s a d x a = b c x d = e f 0 1
constrfin.1 φ N ω
Assertion constrfin φ C N Fin

Proof

Step Hyp Ref Expression
1 constr0.1 C = rec s V x | a s b s c s d s t r x = a + t b a x = c + r d c b a d c 0 a s b s c s e s f s t x = a + t b a x c = e f a s b s c s d s e s f s a d x a = b c x d = e f 0 1
2 constrfin.1 φ N ω
3 fveq2 m = C m = C
4 3 eleq1d m = C m Fin C Fin
5 fveq2 m = n C m = C n
6 5 eleq1d m = n C m Fin C n Fin
7 fveq2 m = suc n C m = C suc n
8 7 eleq1d m = suc n C m Fin C suc n Fin
9 fveq2 m = N C m = C N
10 9 eleq1d m = N C m Fin C N Fin
11 1 constr0 C = 0 1
12 prfi 0 1 Fin
13 11 12 eqeltri C Fin
14 nfv x n ω C n Fin
15 nfcv _ x C suc n
16 nfrab1 _ x x | a C n b C n c C n d C n t r x = a + t b a x = c + r d c b a d c 0 a C n b C n c C n e C n f C n t x = a + t b a x c = e f a C n b C n c C n d C n e C n f C n a d x a = b c x d = e f
17 nnon n ω n On
18 17 adantr n ω C n Fin n On
19 eqid C n = C n
20 1 18 19 constrsuc n ω C n Fin x C suc n x a C n b C n c C n d C n t r x = a + t b a x = c + r d c b a d c 0 a C n b C n c C n e C n f C n t x = a + t b a x c = e f a C n b C n c C n d C n e C n f C n a d x a = b c x d = e f
21 rabid x x | a C n b C n c C n d C n t r x = a + t b a x = c + r d c b a d c 0 a C n b C n c C n e C n f C n t x = a + t b a x c = e f a C n b C n c C n d C n e C n f C n a d x a = b c x d = e f x a C n b C n c C n d C n t r x = a + t b a x = c + r d c b a d c 0 a C n b C n c C n e C n f C n t x = a + t b a x c = e f a C n b C n c C n d C n e C n f C n a d x a = b c x d = e f
22 20 21 bitr4di n ω C n Fin x C suc n x x | a C n b C n c C n d C n t r x = a + t b a x = c + r d c b a d c 0 a C n b C n c C n e C n f C n t x = a + t b a x c = e f a C n b C n c C n d C n e C n f C n a d x a = b c x d = e f
23 14 15 16 22 eqrd n ω C n Fin C suc n = x | a C n b C n c C n d C n t r x = a + t b a x = c + r d c b a d c 0 a C n b C n c C n e C n f C n t x = a + t b a x c = e f a C n b C n c C n d C n e C n f C n a d x a = b c x d = e f
24 3unrab x | a C n b C n c C n d C n t r x = a + t b a x = c + r d c b a d c 0 x | a C n b C n c C n e C n f C n t x = a + t b a x c = e f x | a C n b C n c C n d C n e C n f C n a d x a = b c x d = e f = x | a C n b C n c C n d C n t r x = a + t b a x = c + r d c b a d c 0 a C n b C n c C n e C n f C n t x = a + t b a x c = e f a C n b C n c C n d C n e C n f C n a d x a = b c x d = e f
25 23 24 eqtr4di n ω C n Fin C suc n = x | a C n b C n c C n d C n t r x = a + t b a x = c + r d c b a d c 0 x | a C n b C n c C n e C n f C n t x = a + t b a x c = e f x | a C n b C n c C n d C n e C n f C n a d x a = b c x d = e f
26 simpr n ω C n Fin C n Fin
27 26 adantr n ω C n Fin a C n C n Fin
28 27 adantr n ω C n Fin a C n b C n C n Fin
29 28 adantr n ω C n Fin a C n b C n c C n C n Fin
30 snfi a + a c d c a c d c b a d c b a d c b a Fin
31 30 a1i n ω C n Fin a C n b C n c C n d C n a + a c d c a c d c b a d c b a d c b a Fin
32 1 17 constrsscn n ω C n
33 32 ad9antr n ω C n Fin a C n b C n c C n d C n x t r x = a + t b a x = c + r d c b a d c 0 C n
34 simp-8r n ω C n Fin a C n b C n c C n d C n x t r x = a + t b a x = c + r d c b a d c 0 a C n
35 simp-7r n ω C n Fin a C n b C n c C n d C n x t r x = a + t b a x = c + r d c b a d c 0 b C n
36 simp-6r n ω C n Fin a C n b C n c C n d C n x t r x = a + t b a x = c + r d c b a d c 0 c C n
37 simp-5r n ω C n Fin a C n b C n c C n d C n x t r x = a + t b a x = c + r d c b a d c 0 d C n
38 simpllr n ω C n Fin a C n b C n c C n d C n x t r x = a + t b a x = c + r d c b a d c 0 t
39 simplr n ω C n Fin a C n b C n c C n d C n x t r x = a + t b a x = c + r d c b a d c 0 r
40 simpr1 n ω C n Fin a C n b C n c C n d C n x t r x = a + t b a x = c + r d c b a d c 0 x = a + t b a
41 simpr2 n ω C n Fin a C n b C n c C n d C n x t r x = a + t b a x = c + r d c b a d c 0 x = c + r d c
42 simpr3 n ω C n Fin a C n b C n c C n d C n x t r x = a + t b a x = c + r d c b a d c 0 b a d c 0
43 eqid a + a c d c a c d c b a d c b a d c b a = a + a c d c a c d c b a d c b a d c b a
44 33 34 35 36 37 38 39 40 41 42 43 constrrtll n ω C n Fin a C n b C n c C n d C n x t r x = a + t b a x = c + r d c b a d c 0 x = a + a c d c a c d c b a d c b a d c b a
45 44 r19.29an n ω C n Fin a C n b C n c C n d C n x t r x = a + t b a x = c + r d c b a d c 0 x = a + a c d c a c d c b a d c b a d c b a
46 45 r19.29an n ω C n Fin a C n b C n c C n d C n x t r x = a + t b a x = c + r d c b a d c 0 x = a + a c d c a c d c b a d c b a d c b a
47 46 ex n ω C n Fin a C n b C n c C n d C n x t r x = a + t b a x = c + r d c b a d c 0 x = a + a c d c a c d c b a d c b a d c b a
48 47 ralrimiva n ω C n Fin a C n b C n c C n d C n x t r x = a + t b a x = c + r d c b a d c 0 x = a + a c d c a c d c b a d c b a d c b a
49 rabsssn x | t r x = a + t b a x = c + r d c b a d c 0 a + a c d c a c d c b a d c b a d c b a x t r x = a + t b a x = c + r d c b a d c 0 x = a + a c d c a c d c b a d c b a d c b a
50 48 49 sylibr n ω C n Fin a C n b C n c C n d C n x | t r x = a + t b a x = c + r d c b a d c 0 a + a c d c a c d c b a d c b a d c b a
51 31 50 ssfid n ω C n Fin a C n b C n c C n d C n x | t r x = a + t b a x = c + r d c b a d c 0 Fin
52 29 51 rabrexfi n ω C n Fin a C n b C n c C n x | d C n t r x = a + t b a x = c + r d c b a d c 0 Fin
53 28 52 rabrexfi n ω C n Fin a C n b C n x | c C n d C n t r x = a + t b a x = c + r d c b a d c 0 Fin
54 27 53 rabrexfi n ω C n Fin a C n x | b C n c C n d C n t r x = a + t b a x = c + r d c b a d c 0 Fin
55 26 54 rabrexfi n ω C n Fin x | a C n b C n c C n d C n t r x = a + t b a x = c + r d c b a d c 0 Fin
56 29 adantr n ω C n Fin a C n b C n c C n e C n C n Fin
57 snfi a Fin
58 57 a1i n ω C n Fin a C n b C n c C n e C n f C n a = b a Fin
59 32 ad10antr n ω C n Fin a C n b C n c C n e C n f C n a = b x t x = a + t b a x c = e f C n
60 simp-9r n ω C n Fin a C n b C n c C n e C n f C n a = b x t x = a + t b a x c = e f a C n
61 simp-8r n ω C n Fin a C n b C n c C n e C n f C n a = b x t x = a + t b a x c = e f b C n
62 simp-7r n ω C n Fin a C n b C n c C n e C n f C n a = b x t x = a + t b a x c = e f c C n
63 simp-6r n ω C n Fin a C n b C n c C n e C n f C n a = b x t x = a + t b a x c = e f e C n
64 simp-5r n ω C n Fin a C n b C n c C n e C n f C n a = b x t x = a + t b a x c = e f f C n
65 simplr n ω C n Fin a C n b C n c C n e C n f C n a = b x t x = a + t b a x c = e f t
66 simprl n ω C n Fin a C n b C n c C n e C n f C n a = b x t x = a + t b a x c = e f x = a + t b a
67 simprr n ω C n Fin a C n b C n c C n e C n f C n a = b x t x = a + t b a x c = e f x c = e f
68 simp-4r n ω C n Fin a C n b C n c C n e C n f C n a = b x t x = a + t b a x c = e f a = b
69 59 60 61 62 63 64 65 66 67 68 constrrtlc2 n ω C n Fin a C n b C n c C n e C n f C n a = b x t x = a + t b a x c = e f x = a
70 69 r19.29an n ω C n Fin a C n b C n c C n e C n f C n a = b x t x = a + t b a x c = e f x = a
71 70 ex n ω C n Fin a C n b C n c C n e C n f C n a = b x t x = a + t b a x c = e f x = a
72 71 ralrimiva n ω C n Fin a C n b C n c C n e C n f C n a = b x t x = a + t b a x c = e f x = a
73 rabsssn x | t x = a + t b a x c = e f a x t x = a + t b a x c = e f x = a
74 72 73 sylibr n ω C n Fin a C n b C n c C n e C n f C n a = b x | t x = a + t b a x c = e f a
75 58 74 ssfid n ω C n Fin a C n b C n c C n e C n f C n a = b x | t x = a + t b a x c = e f Fin
76 prfi - a a b a b a - c - c b a b a b a b a + a a b a b a - c - c b a b a b a b a 2 4 1 c a - a b a b a - c + e f e f b a b a 2 1 - a a b a b a - c - c b a b a b a b a - a a b a b a - c - c b a b a b a b a 2 4 1 c a - a b a b a - c + e f e f b a b a 2 1 Fin
77 76 a1i n ω C n Fin a C n b C n c C n e C n f C n a b - a a b a b a - c - c b a b a b a b a + a a b a b a - c - c b a b a b a b a 2 4 1 c a - a b a b a - c + e f e f b a b a 2 1 - a a b a b a - c - c b a b a b a b a - a a b a b a - c - c b a b a b a b a 2 4 1 c a - a b a b a - c + e f e f b a b a 2 1 Fin
78 simpllr n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f x
79 1cnd n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f 1
80 ax-1ne0 1 0
81 80 a1i n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f 1 0
82 32 ad10antr n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f C n
83 simp-9r n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f a C n
84 82 83 sseldd n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f a
85 84 cjcld n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f a
86 simp-8r n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f b C n
87 82 86 sseldd n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f b
88 87 cjcld n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f b
89 88 85 subcld n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f b a
90 87 84 subcld n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f b a
91 simp-4r n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f a b
92 91 necomd n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f b a
93 87 84 92 subne0d n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f b a 0
94 89 90 93 divcld n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f b a b a
95 84 94 mulcld n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f a b a b a
96 85 95 subcld n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f a a b a b a
97 simp-7r n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f c C n
98 82 97 sseldd n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f c
99 98 cjcld n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f c
100 96 99 subcld n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f a - a b a b a - c
101 98 94 mulcld n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f c b a b a
102 100 101 subcld n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f a a b a b a - c - c b a b a
103 simp-6r n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f e C n
104 simp-5r n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f f C n
105 simplr n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f t
106 simprl n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f x = a + t b a
107 simprr n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f x c = e f
108 eqid b a b a = b a b a
109 eqid a a b a b a - c - c b a b a b a b a = a a b a b a - c - c b a b a b a b a
110 eqid c a - a b a b a - c + e f e f b a b a = c a - a b a b a - c + e f e f b a b a
111 82 83 86 97 103 104 105 106 107 108 109 110 91 constrrtlc1 n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f x 2 + a a b a b a - c - c b a b a b a b a x + c a - a b a b a - c + e f e f b a b a = 0 b a b a 0
112 111 simprd n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f b a b a 0
113 102 94 112 divcld n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f a a b a b a - c - c b a b a b a b a
114 98 100 mulcld n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f c a - a b a b a - c
115 82 103 sseldd n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f e
116 82 104 sseldd n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f f
117 115 116 subcld n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f e f
118 115 cjcld n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f e
119 116 cjcld n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f f
120 118 119 subcld n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f e f
121 117 120 mulcld n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f e f e f
122 114 121 addcld n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f c a - a b a b a - c + e f e f
123 122 negcld n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f c a - a b a b a - c + e f e f
124 123 94 112 divcld n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f c a - a b a b a - c + e f e f b a b a
125 78 sqcld n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f x 2
126 125 mullidd n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f 1 x 2 = x 2
127 126 oveq1d n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f 1 x 2 + a a b a b a - c - c b a b a b a b a x + c a - a b a b a - c + e f e f b a b a = x 2 + a a b a b a - c - c b a b a b a b a x + c a - a b a b a - c + e f e f b a b a
128 111 simpld n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f x 2 + a a b a b a - c - c b a b a b a b a x + c a - a b a b a - c + e f e f b a b a = 0
129 127 128 eqtrd n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f 1 x 2 + a a b a b a - c - c b a b a b a b a x + c a - a b a b a - c + e f e f b a b a = 0
130 78 79 81 113 124 129 quad3d n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f x = - a a b a b a - c - c b a b a b a b a + a a b a b a - c - c b a b a b a b a 2 4 1 c a - a b a b a - c + e f e f b a b a 2 1 x = - a a b a b a - c - c b a b a b a b a - a a b a b a - c - c b a b a b a b a 2 4 1 c a - a b a b a - c + e f e f b a b a 2 1
131 130 r19.29an n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f x = - a a b a b a - c - c b a b a b a b a + a a b a b a - c - c b a b a b a b a 2 4 1 c a - a b a b a - c + e f e f b a b a 2 1 x = - a a b a b a - c - c b a b a b a b a - a a b a b a - c - c b a b a b a b a 2 4 1 c a - a b a b a - c + e f e f b a b a 2 1
132 131 ex n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f x = - a a b a b a - c - c b a b a b a b a + a a b a b a - c - c b a b a b a b a 2 4 1 c a - a b a b a - c + e f e f b a b a 2 1 x = - a a b a b a - c - c b a b a b a b a - a a b a b a - c - c b a b a b a b a 2 4 1 c a - a b a b a - c + e f e f b a b a 2 1
133 132 ralrimiva n ω C n Fin a C n b C n c C n e C n f C n a b x t x = a + t b a x c = e f x = - a a b a b a - c - c b a b a b a b a + a a b a b a - c - c b a b a b a b a 2 4 1 c a - a b a b a - c + e f e f b a b a 2 1 x = - a a b a b a - c - c b a b a b a b a - a a b a b a - c - c b a b a b a b a 2 4 1 c a - a b a b a - c + e f e f b a b a 2 1
134 rabsspr x | t x = a + t b a x c = e f - a a b a b a - c - c b a b a b a b a + a a b a b a - c - c b a b a b a b a 2 4 1 c a - a b a b a - c + e f e f b a b a 2 1 - a a b a b a - c - c b a b a b a b a - a a b a b a - c - c b a b a b a b a 2 4 1 c a - a b a b a - c + e f e f b a b a 2 1 x t x = a + t b a x c = e f x = - a a b a b a - c - c b a b a b a b a + a a b a b a - c - c b a b a b a b a 2 4 1 c a - a b a b a - c + e f e f b a b a 2 1 x = - a a b a b a - c - c b a b a b a b a - a a b a b a - c - c b a b a b a b a 2 4 1 c a - a b a b a - c + e f e f b a b a 2 1
135 133 134 sylibr n ω C n Fin a C n b C n c C n e C n f C n a b x | t x = a + t b a x c = e f - a a b a b a - c - c b a b a b a b a + a a b a b a - c - c b a b a b a b a 2 4 1 c a - a b a b a - c + e f e f b a b a 2 1 - a a b a b a - c - c b a b a b a b a - a a b a b a - c - c b a b a b a b a 2 4 1 c a - a b a b a - c + e f e f b a b a 2 1
136 77 135 ssfid n ω C n Fin a C n b C n c C n e C n f C n a b x | t x = a + t b a x c = e f Fin
137 exmidne a = b a b
138 137 a1i n ω C n Fin a C n b C n c C n e C n f C n a = b a b
139 75 136 138 mpjaodan n ω C n Fin a C n b C n c C n e C n f C n x | t x = a + t b a x c = e f Fin
140 56 139 rabrexfi n ω C n Fin a C n b C n c C n e C n x | f C n t x = a + t b a x c = e f Fin
141 29 140 rabrexfi n ω C n Fin a C n b C n c C n x | e C n f C n t x = a + t b a x c = e f Fin
142 28 141 rabrexfi n ω C n Fin a C n b C n x | c C n e C n f C n t x = a + t b a x c = e f Fin
143 27 142 rabrexfi n ω C n Fin a C n x | b C n c C n e C n f C n t x = a + t b a x c = e f Fin
144 26 143 rabrexfi n ω C n Fin x | a C n b C n c C n e C n f C n t x = a + t b a x c = e f Fin
145 55 144 unfid n ω C n Fin x | a C n b C n c C n d C n t r x = a + t b a x = c + r d c b a d c 0 x | a C n b C n c C n e C n f C n t x = a + t b a x c = e f Fin
146 29 adantr n ω C n Fin a C n b C n c C n d C n C n Fin
147 146 adantr n ω C n Fin a C n b C n c C n d C n e C n C n Fin
148 prfi - e f e f - d d + a - b c b c a d + a d a + e f e f - d d + a - b c b c a d + a d a 2 4 1 a d a - b c b c d - d d a e f e f a d a 2 1 - e f e f - d d + a - b c b c a d + a d a - e f e f - d d + a - b c b c a d + a d a 2 4 1 a d a - b c b c d - d d a e f e f a d a 2 1 Fin
149 148 a1i n ω C n Fin a C n b C n c C n d C n e C n f C n - e f e f - d d + a - b c b c a d + a d a + e f e f - d d + a - b c b c a d + a d a 2 4 1 a d a - b c b c d - d d a e f e f a d a 2 1 - e f e f - d d + a - b c b c a d + a d a - e f e f - d d + a - b c b c a d + a d a 2 4 1 a d a - b c b c d - d d a e f e f a d a 2 1 Fin
150 simplr n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f x
151 1cnd n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f 1
152 80 a1i n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f 1 0
153 32 ad9antr n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f C n
154 simp-4r n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f e C n
155 153 154 sseldd n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f e
156 simpllr n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f f C n
157 153 156 sseldd n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f f
158 155 157 subcld n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f e f
159 158 cjcld n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f e f
160 158 159 mulcld n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f e f e f
161 simp-5r n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f d C n
162 153 161 sseldd n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f d
163 162 cjcld n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f d
164 simp-8r n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f a C n
165 153 164 sseldd n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f a
166 162 165 addcld n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f d + a
167 163 166 mulcld n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f d d + a
168 160 167 subcld n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f e f e f d d + a
169 simp-7r n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f b C n
170 153 169 sseldd n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f b
171 simp-6r n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f c C n
172 153 171 sseldd n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f c
173 170 172 subcld n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f b c
174 173 cjcld n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f b c
175 173 174 mulcld n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f b c b c
176 165 cjcld n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f a
177 176 166 mulcld n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f a d + a
178 175 177 subcld n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f b c b c a d + a
179 168 178 subcld n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f e f e f - d d + a - b c b c a d + a
180 163 176 subcld n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f d a
181 162 165 cjsubd n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f d a = d a
182 162 165 subcld n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f d a
183 simpr1 n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f a d
184 183 necomd n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f d a
185 162 165 184 subne0d n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f d a 0
186 182 185 cjne0d n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f d a 0
187 181 186 eqnetrrd n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f d a 0
188 179 180 187 divcld n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f e f e f - d d + a - b c b c a d + a d a
189 162 165 mulcld n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f d a
190 176 189 mulcld n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f a d a
191 175 162 mulcld n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f b c b c d
192 190 191 subcld n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f a d a b c b c d
193 163 189 mulcld n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f d d a
194 160 165 mulcld n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f e f e f a
195 193 194 subcld n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f d d a e f e f a
196 192 195 subcld n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f a d a - b c b c d - d d a e f e f a
197 196 180 187 divcld n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f a d a - b c b c d - d d a e f e f a d a
198 197 negcld n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f a d a - b c b c d - d d a e f e f a d a
199 150 sqcld n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f x 2
200 199 mullidd n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f 1 x 2 = x 2
201 200 oveq1d n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f 1 x 2 + e f e f - d d + a - b c b c a d + a d a x + a d a - b c b c d - d d a e f e f a d a = x 2 + e f e f - d d + a - b c b c a d + a d a x + a d a - b c b c d - d d a e f e f a d a
202 simpr2 n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f x a = b c
203 simpr3 n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f x d = e f
204 eqid b c b c = b c b c
205 eqid e f e f = e f e f
206 eqid e f e f - d d + a - b c b c a d + a d a = e f e f - d d + a - b c b c a d + a d a
207 eqid a d a - b c b c d - d d a e f e f a d a = a d a - b c b c d - d d a e f e f a d a
208 153 164 169 171 161 154 156 150 183 202 203 204 205 206 207 constrrtcc n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f x 2 + e f e f - d d + a - b c b c a d + a d a x + a d a - b c b c d - d d a e f e f a d a = 0
209 201 208 eqtrd n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f 1 x 2 + e f e f - d d + a - b c b c a d + a d a x + a d a - b c b c d - d d a e f e f a d a = 0
210 150 151 152 188 198 209 quad3d n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f x = - e f e f - d d + a - b c b c a d + a d a + e f e f - d d + a - b c b c a d + a d a 2 4 1 a d a - b c b c d - d d a e f e f a d a 2 1 x = - e f e f - d d + a - b c b c a d + a d a - e f e f - d d + a - b c b c a d + a d a 2 4 1 a d a - b c b c d - d d a e f e f a d a 2 1
211 210 ex n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f x = - e f e f - d d + a - b c b c a d + a d a + e f e f - d d + a - b c b c a d + a d a 2 4 1 a d a - b c b c d - d d a e f e f a d a 2 1 x = - e f e f - d d + a - b c b c a d + a d a - e f e f - d d + a - b c b c a d + a d a 2 4 1 a d a - b c b c d - d d a e f e f a d a 2 1
212 211 ralrimiva n ω C n Fin a C n b C n c C n d C n e C n f C n x a d x a = b c x d = e f x = - e f e f - d d + a - b c b c a d + a d a + e f e f - d d + a - b c b c a d + a d a 2 4 1 a d a - b c b c d - d d a e f e f a d a 2 1 x = - e f e f - d d + a - b c b c a d + a d a - e f e f - d d + a - b c b c a d + a d a 2 4 1 a d a - b c b c d - d d a e f e f a d a 2 1
213 rabsspr x | a d x a = b c x d = e f - e f e f - d d + a - b c b c a d + a d a + e f e f - d d + a - b c b c a d + a d a 2 4 1 a d a - b c b c d - d d a e f e f a d a 2 1 - e f e f - d d + a - b c b c a d + a d a - e f e f - d d + a - b c b c a d + a d a 2 4 1 a d a - b c b c d - d d a e f e f a d a 2 1 x a d x a = b c x d = e f x = - e f e f - d d + a - b c b c a d + a d a + e f e f - d d + a - b c b c a d + a d a 2 4 1 a d a - b c b c d - d d a e f e f a d a 2 1 x = - e f e f - d d + a - b c b c a d + a d a - e f e f - d d + a - b c b c a d + a d a 2 4 1 a d a - b c b c d - d d a e f e f a d a 2 1
214 212 213 sylibr n ω C n Fin a C n b C n c C n d C n e C n f C n x | a d x a = b c x d = e f - e f e f - d d + a - b c b c a d + a d a + e f e f - d d + a - b c b c a d + a d a 2 4 1 a d a - b c b c d - d d a e f e f a d a 2 1 - e f e f - d d + a - b c b c a d + a d a - e f e f - d d + a - b c b c a d + a d a 2 4 1 a d a - b c b c d - d d a e f e f a d a 2 1
215 149 214 ssfid n ω C n Fin a C n b C n c C n d C n e C n f C n x | a d x a = b c x d = e f Fin
216 147 215 rabrexfi n ω C n Fin a C n b C n c C n d C n e C n x | f C n a d x a = b c x d = e f Fin
217 146 216 rabrexfi n ω C n Fin a C n b C n c C n d C n x | e C n f C n a d x a = b c x d = e f Fin
218 29 217 rabrexfi n ω C n Fin a C n b C n c C n x | d C n e C n f C n a d x a = b c x d = e f Fin
219 28 218 rabrexfi n ω C n Fin a C n b C n x | c C n d C n e C n f C n a d x a = b c x d = e f Fin
220 27 219 rabrexfi n ω C n Fin a C n x | b C n c C n d C n e C n f C n a d x a = b c x d = e f Fin
221 26 220 rabrexfi n ω C n Fin x | a C n b C n c C n d C n e C n f C n a d x a = b c x d = e f Fin
222 145 221 unfid n ω C n Fin x | a C n b C n c C n d C n t r x = a + t b a x = c + r d c b a d c 0 x | a C n b C n c C n e C n f C n t x = a + t b a x c = e f x | a C n b C n c C n d C n e C n f C n a d x a = b c x d = e f Fin
223 25 222 eqeltrd n ω C n Fin C suc n Fin
224 223 ex n ω C n Fin C suc n Fin
225 4 6 8 10 13 224 finds N ω C N Fin
226 2 225 syl φ C N Fin