Metamath Proof Explorer


Theorem knoppcnlem5

Description: Lemma for knoppcn . (Contributed by Asger C. Ipsen, 4-Apr-2021) (Revised by Asger C. Ipsen, 5-Jul-2021)

Ref Expression
Hypotheses knoppcnlem5.t T=xx+12x
knoppcnlem5.f F=yn0CnT2 Nny
knoppcnlem5.n φN
knoppcnlem5.1 φC
Assertion knoppcnlem5 φm0zFzm:0

Proof

Step Hyp Ref Expression
1 knoppcnlem5.t T=xx+12x
2 knoppcnlem5.f F=yn0CnT2 Nny
3 knoppcnlem5.n φN
4 knoppcnlem5.1 φC
5 3 ad2antrr φm0zN
6 4 ad2antrr φm0zC
7 simpr φm0zz
8 simplr φm0zm0
9 1 2 5 6 7 8 knoppcnlem3 φm0zFzm
10 9 recnd φm0zFzm
11 10 fmpttd φm0zFzm:
12 cnex V
13 reex V
14 12 13 pm3.2i VV
15 elmapg VVzFzmzFzm:
16 14 15 ax-mp zFzmzFzm:
17 11 16 sylibr φm0zFzm
18 17 fmpttd φm0zFzm:0