Theorem indlt ≪ | index | src | ≫ 

theorem indlt (G: wff) {x y: nat} (a: nat) (px: wff x) (p0 pa py ps: wff y):
  $ x = a -> (px <-> pa) $ >
  $ x = 0 -> (px <-> p0) $ >
  $ x = y -> (px <-> py) $ >
  $ x = suc y -> (px <-> ps) $ >
  $ G -> p0 $ >
  $ G /\ y < a /\ py -> ps $ >
  $ G -> pa $;
StepHypRefExpression
1 leid 
a <= a
2 leeq1 
x = a -> (x <= a <-> a <= a)
3 hyp ha 
x = a -> (px <-> pa)
4 2, 3 imeqd 
x = a -> (x <= a -> px <-> a <= a -> pa)
5 leeq1 
x = 0 -> (x <= a <-> 0 <= a)
6 hyp h0 
x = 0 -> (px <-> p0)
7 5, 6 imeqd 
x = 0 -> (x <= a -> px <-> 0 <= a -> p0)
8 leeq1 
x = y -> (x <= a <-> y <= a)
9 hyp hy 
x = y -> (px <-> py)
10 8, 9 imeqd 
x = y -> (x <= a -> px <-> y <= a -> py)
11 leeq1 
x = suc y -> (x <= a <-> suc y <= a)
12 hyp hs 
x = suc y -> (px <-> ps)
13 11, 12 imeqd 
x = suc y -> (x <= a -> px <-> suc y <= a -> ps)
14 hyp h1 
G -> p0
15 14 a1d 
G -> 0 <= a -> p0
16 ltle 
y < a -> y <= a
17 16 imim1i 
(y <= a -> py) -> y < a -> py
18 hyp h2 
G /\ y < a /\ py -> ps
19 18 exp 
G /\ y < a -> py -> ps
20 19 exp 
G -> y < a -> py -> ps
21 20 a2d 
G -> (y < a -> py) -> y < a -> ps
22 21 conv lt 
G -> (y < a -> py) -> suc y <= a -> ps
23 17, 22 syl5 
G -> (y <= a -> py) -> suc y <= a -> ps
24 23 imp 
G /\ (y <= a -> py) -> suc y <= a -> ps
25 4, 7, 10, 13, 15, 24 indd 
G -> a <= a -> pa
26 1, 25 mpi 
G -> pa

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_peano (peano2, peano5, addeq, add0, addS)