Step | Hyp | Ref
| Expression |
1 | | nfmpt1 5249 |
. . . . . . 7
β’
β²π‘(π‘ β (β€ βm
(1...π)) β¦ π΄) |
2 | 1 | nfel1 2913 |
. . . . . 6
β’
β²π‘(π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π)) |
3 | | nfmpt1 5249 |
. . . . . . 7
β’
β²π‘(π‘ β (β€ βm
(1...π)) β¦ π΅) |
4 | 3 | nfel1 2913 |
. . . . . 6
β’
β²π‘(π‘ β (β€
βm (1...π))
β¦ π΅) β
(mzPolyβ(1...π)) |
5 | 2, 4 | nfan 1894 |
. . . . 5
β’
β²π‘((π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π))
β§ (π‘ β (β€
βm (1...π))
β¦ π΅) β
(mzPolyβ(1...π))) |
6 | | mzpf 42057 |
. . . . . . . . . . 11
β’ ((π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π))
β (π‘ β (β€
βm (1...π))
β¦ π΄):(β€
βm (1...π))βΆβ€) |
7 | 6 | ad2antrr 723 |
. . . . . . . . . 10
β’ ((((π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π))
β§ (π‘ β (β€
βm (1...π))
β¦ π΅) β
(mzPolyβ(1...π)))
β§ π‘ β
(β0 βm (1...π))) β (π‘ β (β€ βm
(1...π)) β¦ π΄):(β€ βm
(1...π))βΆβ€) |
8 | | zex 12571 |
. . . . . . . . . . . . 13
β’ β€
β V |
9 | | nn0ssz 12585 |
. . . . . . . . . . . . 13
β’
β0 β β€ |
10 | | mapss 8885 |
. . . . . . . . . . . . 13
β’ ((β€
β V β§ β0 β β€) β (β0
βm (1...π))
β (β€ βm (1...π))) |
11 | 8, 9, 10 | mp2an 689 |
. . . . . . . . . . . 12
β’
(β0 βm (1...π)) β (β€ βm
(1...π)) |
12 | 11 | sseli 3973 |
. . . . . . . . . . 11
β’ (π‘ β (β0
βm (1...π))
β π‘ β (β€
βm (1...π))) |
13 | 12 | adantl 481 |
. . . . . . . . . 10
β’ ((((π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π))
β§ (π‘ β (β€
βm (1...π))
β¦ π΅) β
(mzPolyβ(1...π)))
β§ π‘ β
(β0 βm (1...π))) β π‘ β (β€ βm
(1...π))) |
14 | | mptfcl 42041 |
. . . . . . . . . 10
β’ ((π‘ β (β€
βm (1...π))
β¦ π΄):(β€
βm (1...π))βΆβ€ β (π‘ β (β€ βm
(1...π)) β π΄ β
β€)) |
15 | 7, 13, 14 | sylc 65 |
. . . . . . . . 9
β’ ((((π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π))
β§ (π‘ β (β€
βm (1...π))
β¦ π΅) β
(mzPolyβ(1...π)))
β§ π‘ β
(β0 βm (1...π))) β π΄ β β€) |
16 | 15 | zcnd 12671 |
. . . . . . . 8
β’ ((((π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π))
β§ (π‘ β (β€
βm (1...π))
β¦ π΅) β
(mzPolyβ(1...π)))
β§ π‘ β
(β0 βm (1...π))) β π΄ β β) |
17 | | mzpf 42057 |
. . . . . . . . . . 11
β’ ((π‘ β (β€
βm (1...π))
β¦ π΅) β
(mzPolyβ(1...π))
β (π‘ β (β€
βm (1...π))
β¦ π΅):(β€
βm (1...π))βΆβ€) |
18 | 17 | ad2antlr 724 |
. . . . . . . . . 10
β’ ((((π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π))
β§ (π‘ β (β€
βm (1...π))
β¦ π΅) β
(mzPolyβ(1...π)))
β§ π‘ β
(β0 βm (1...π))) β (π‘ β (β€ βm
(1...π)) β¦ π΅):(β€ βm
(1...π))βΆβ€) |
19 | | mptfcl 42041 |
. . . . . . . . . 10
β’ ((π‘ β (β€
βm (1...π))
β¦ π΅):(β€
βm (1...π))βΆβ€ β (π‘ β (β€ βm
(1...π)) β π΅ β
β€)) |
20 | 18, 13, 19 | sylc 65 |
. . . . . . . . 9
β’ ((((π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π))
β§ (π‘ β (β€
βm (1...π))
β¦ π΅) β
(mzPolyβ(1...π)))
β§ π‘ β
(β0 βm (1...π))) β π΅ β β€) |
21 | 20 | zcnd 12671 |
. . . . . . . 8
β’ ((((π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π))
β§ (π‘ β (β€
βm (1...π))
β¦ π΅) β
(mzPolyβ(1...π)))
β§ π‘ β
(β0 βm (1...π))) β π΅ β β) |
22 | 16, 21 | subeq0ad 11585 |
. . . . . . 7
β’ ((((π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π))
β§ (π‘ β (β€
βm (1...π))
β¦ π΅) β
(mzPolyβ(1...π)))
β§ π‘ β
(β0 βm (1...π))) β ((π΄ β π΅) = 0 β π΄ = π΅)) |
23 | 22 | bicomd 222 |
. . . . . 6
β’ ((((π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π))
β§ (π‘ β (β€
βm (1...π))
β¦ π΅) β
(mzPolyβ(1...π)))
β§ π‘ β
(β0 βm (1...π))) β (π΄ = π΅ β (π΄ β π΅) = 0)) |
24 | 23 | ex 412 |
. . . . 5
β’ (((π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π))
β§ (π‘ β (β€
βm (1...π))
β¦ π΅) β
(mzPolyβ(1...π)))
β (π‘ β
(β0 βm (1...π)) β (π΄ = π΅ β (π΄ β π΅) = 0))) |
25 | 5, 24 | ralrimi 3248 |
. . . 4
β’ (((π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π))
β§ (π‘ β (β€
βm (1...π))
β¦ π΅) β
(mzPolyβ(1...π)))
β βπ‘ β
(β0 βm (1...π))(π΄ = π΅ β (π΄ β π΅) = 0)) |
26 | | rabbi 3456 |
. . . 4
β’
(βπ‘ β
(β0 βm (1...π))(π΄ = π΅ β (π΄ β π΅) = 0) β {π‘ β (β0
βm (1...π))
β£ π΄ = π΅} = {π‘ β (β0
βm (1...π))
β£ (π΄ β π΅) = 0}) |
27 | 25, 26 | sylib 217 |
. . 3
β’ (((π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π))
β§ (π‘ β (β€
βm (1...π))
β¦ π΅) β
(mzPolyβ(1...π)))
β {π‘ β
(β0 βm (1...π)) β£ π΄ = π΅} = {π‘ β (β0
βm (1...π))
β£ (π΄ β π΅) = 0}) |
28 | 27 | 3adant1 1127 |
. 2
β’ ((π β β0
β§ (π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π))
β§ (π‘ β (β€
βm (1...π))
β¦ π΅) β
(mzPolyβ(1...π)))
β {π‘ β
(β0 βm (1...π)) β£ π΄ = π΅} = {π‘ β (β0
βm (1...π))
β£ (π΄ β π΅) = 0}) |
29 | | simp1 1133 |
. . 3
β’ ((π β β0
β§ (π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π))
β§ (π‘ β (β€
βm (1...π))
β¦ π΅) β
(mzPolyβ(1...π)))
β π β
β0) |
30 | | mzpsubmpt 42064 |
. . . 4
β’ (((π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π))
β§ (π‘ β (β€
βm (1...π))
β¦ π΅) β
(mzPolyβ(1...π)))
β (π‘ β (β€
βm (1...π))
β¦ (π΄ β π΅)) β
(mzPolyβ(1...π))) |
31 | 30 | 3adant1 1127 |
. . 3
β’ ((π β β0
β§ (π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π))
β§ (π‘ β (β€
βm (1...π))
β¦ π΅) β
(mzPolyβ(1...π)))
β (π‘ β (β€
βm (1...π))
β¦ (π΄ β π΅)) β
(mzPolyβ(1...π))) |
32 | | eq0rabdioph 42097 |
. . 3
β’ ((π β β0
β§ (π‘ β (β€
βm (1...π))
β¦ (π΄ β π΅)) β
(mzPolyβ(1...π)))
β {π‘ β
(β0 βm (1...π)) β£ (π΄ β π΅) = 0} β (Diophβπ)) |
33 | 29, 31, 32 | syl2anc 583 |
. 2
β’ ((π β β0
β§ (π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π))
β§ (π‘ β (β€
βm (1...π))
β¦ π΅) β
(mzPolyβ(1...π)))
β {π‘ β
(β0 βm (1...π)) β£ (π΄ β π΅) = 0} β (Diophβπ)) |
34 | 28, 33 | eqeltrd 2827 |
1
β’ ((π β β0
β§ (π‘ β (β€
βm (1...π))
β¦ π΄) β
(mzPolyβ(1...π))
β§ (π‘ β (β€
βm (1...π))
β¦ π΅) β
(mzPolyβ(1...π)))
β {π‘ β
(β0 βm (1...π)) β£ π΄ = π΅} β (Diophβπ)) |