Theorem n0sind

Description: Principle of Mathematical Induction (inference schema). Compare nnind and finds . (Contributed by Scott Fenton, 17-Mar-2025)

	Ref	Expression
Hypotheses	n0sind.1	No typesetting found for |- ( x = 0s -> ( ph <-> ps ) ) with typecode |-
	n0sind.2	$$⊢x=y\to \left(\phi \leftrightarrow \chi \right)$$
	n0sind.3	No typesetting found for |- ( x = ( y +s 1s ) -> ( ph <-> th ) ) with typecode |-
	n0sind.4	$$⊢x=A\to \left(\phi \leftrightarrow \tau \right)$$
	n0sind.5	$$⊢\psi$$
	n0sind.6	No typesetting found for |- ( y e. NN0_s -> ( ch -> th ) ) with typecode |-
Assertion	n0sind	Could not format assertion : No typesetting found for |- ( A e. NN0_s -> ta ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		n0sind.1	Could not format ( x = 0s -> ( ph <-> ps ) ) : No typesetting found for |- ( x = 0s -> ( ph <-> ps ) ) with typecode |-
2		n0sind.2	$$⊢x=y\to \left(\phi \leftrightarrow \chi \right)$$
3		n0sind.3	Could not format ( x = ( y +s 1s ) -> ( ph <-> th ) ) : No typesetting found for |- ( x = ( y +s 1s ) -> ( ph <-> th ) ) with typecode |-
4		n0sind.4	$$⊢x=A\to \left(\phi \leftrightarrow \tau \right)$$
5		n0sind.5	$$⊢\psi$$
6		n0sind.6	Could not format ( y e. NN0_s -> ( ch -> th ) ) : No typesetting found for |- ( y e. NN0_s -> ( ch -> th ) ) with typecode |-
7		0n0s	Could not format 0s e. NN0_s : No typesetting found for |- 0s e. NN0_s with typecode |-
8	1	elrab	Could not format ( 0s e. { x e. NN0_s | ph } <-> ( 0s e. NN0_s /\ ps ) ) : No typesetting found for |- ( 0s e. { x e. NN0_s | ph } <-> ( 0s e. NN0_s /\ ps ) ) with typecode |-
9	7 5 8	mpbir2an	Could not format 0s e. { x e. NN0_s | ph } : No typesetting found for |- 0s e. { x e. NN0_s | ph } with typecode |-
10		peano2n0s	Could not format ( y e. NN0_s -> ( y +s 1s ) e. NN0_s ) : No typesetting found for |- ( y e. NN0_s -> ( y +s 1s ) e. NN0_s ) with typecode |-
11	6 10	jctild	Could not format ( y e. NN0_s -> ( ch -> ( ( y +s 1s ) e. NN0_s /\ th ) ) ) : No typesetting found for |- ( y e. NN0_s -> ( ch -> ( ( y +s 1s ) e. NN0_s /\ th ) ) ) with typecode |-
12	11	imp	Could not format ( ( y e. NN0_s /\ ch ) -> ( ( y +s 1s ) e. NN0_s /\ th ) ) : No typesetting found for |- ( ( y e. NN0_s /\ ch ) -> ( ( y +s 1s ) e. NN0_s /\ th ) ) with typecode |-
13	2	elrab	Could not format ( y e. { x e. NN0_s | ph } <-> ( y e. NN0_s /\ ch ) ) : No typesetting found for |- ( y e. { x e. NN0_s | ph } <-> ( y e. NN0_s /\ ch ) ) with typecode |-
14	3	elrab	Could not format ( ( y +s 1s ) e. { x e. NN0_s | ph } <-> ( ( y +s 1s ) e. NN0_s /\ th ) ) : No typesetting found for |- ( ( y +s 1s ) e. { x e. NN0_s | ph } <-> ( ( y +s 1s ) e. NN0_s /\ th ) ) with typecode |-
15	12 13 14	3imtr4i	Could not format ( y e. { x e. NN0_s | ph } -> ( y +s 1s ) e. { x e. NN0_s | ph } ) : No typesetting found for |- ( y e. { x e. NN0_s | ph } -> ( y +s 1s ) e. { x e. NN0_s | ph } ) with typecode |-
16	15	rgen	Could not format A. y e. { x e. NN0_s | ph } ( y +s 1s ) e. { x e. NN0_s | ph } : No typesetting found for |- A. y e. { x e. NN0_s | ph } ( y +s 1s ) e. { x e. NN0_s | ph } with typecode |-
17		peano5n0s	Could not format ( ( 0s e. { x e. NN0_s | ph } /\ A. y e. { x e. NN0_s | ph } ( y +s 1s ) e. { x e. NN0_s | ph } ) -> NN0_s C_ { x e. NN0_s | ph } ) : No typesetting found for |- ( ( 0s e. { x e. NN0_s | ph } /\ A. y e. { x e. NN0_s | ph } ( y +s 1s ) e. { x e. NN0_s | ph } ) -> NN0_s C_ { x e. NN0_s | ph } ) with typecode |-
18	9 16 17	mp2an	Could not format NN0_s C_ { x e. NN0_s | ph } : No typesetting found for |- NN0_s C_ { x e. NN0_s | ph } with typecode |-
19	18	sseli	Could not format ( A e. NN0_s -> A e. { x e. NN0_s | ph } ) : No typesetting found for |- ( A e. NN0_s -> A e. { x e. NN0_s | ph } ) with typecode |-
20	4	elrab	Could not format ( A e. { x e. NN0_s | ph } <-> ( A e. NN0_s /\ ta ) ) : No typesetting found for |- ( A e. { x e. NN0_s | ph } <-> ( A e. NN0_s /\ ta ) ) with typecode |-
21	19 20	sylib	Could not format ( A e. NN0_s -> ( A e. NN0_s /\ ta ) ) : No typesetting found for |- ( A e. NN0_s -> ( A e. NN0_s /\ ta ) ) with typecode |-
22	21	simprd	Could not format ( A e. NN0_s -> ta ) : No typesetting found for |- ( A e. NN0_s -> ta ) with typecode |-