Metamath Proof Explorer

Theorem zindbi

Description: Inductively transfer a property to the integers if it holds for zero and passes between adjacent integers in either direction. (Contributed by Stefan O'Rear, 1-Oct-2014)

Ref Expression
Hypotheses zindbi.1 ⊢ ( 𝑦 ∈ ℤ → ( 𝜓 ↔ 𝜒 ) )
zindbi.2 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
zindbi.3 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝜑 ↔ 𝜒 ) )
zindbi.4 ⊢ ( 𝑥 = 0 → ( 𝜑 ↔ 𝜃 ) )
zindbi.5 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
Assertion zindbi ( 𝐴 ∈ ℤ → ( 𝜃 ↔ 𝜏 ) )

Proof

Step Hyp Ref Expression
1 zindbi.1 ⊢ ( 𝑦 ∈ ℤ → ( 𝜓 ↔ 𝜒 ) )
2 zindbi.2 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
3 zindbi.3 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝜑 ↔ 𝜒 ) )
4 zindbi.4 ⊢ ( 𝑥 = 0 → ( 𝜑 ↔ 𝜃 ) )
5 zindbi.5 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
6 c0ex ⊢ 0 ∈ V
7 6 4 sbcie ⊢ ( [ 0 / 𝑥 ] 𝜑 ↔ 𝜃 )
8 0z ⊢ 0 ∈ ℤ
9 eleq1 ⊢ ( 𝑦 = 0 → ( 𝑦 ∈ ℤ ↔ 0 ∈ ℤ ) )
10 breq1 ⊢ ( 𝑦 = 0 → ( 𝑦 ≤ 𝑏 ↔ 0 ≤ 𝑏 ) )
11 9 10 3anbi13d ⊢ ( 𝑦 = 0 → ( ( 𝑦 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝑦 ≤ 𝑏 ) ↔ ( 0 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 0 ≤ 𝑏 ) ) )
12 dfsbcq ⊢ ( 𝑦 = 0 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 0 / 𝑥 ] 𝜑 ) )
13 12 bibi1d ⊢ ( 𝑦 = 0 → ( ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑏 / 𝑥 ] 𝜑 ) ↔ ( [ 0 / 𝑥 ] 𝜑 ↔ [ 𝑏 / 𝑥 ] 𝜑 ) ) )
14 11 13 imbi12d ⊢ ( 𝑦 = 0 → ( ( ( 𝑦 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝑦 ≤ 𝑏 ) → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑏 / 𝑥 ] 𝜑 ) ) ↔ ( ( 0 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 0 ≤ 𝑏 ) → ( [ 0 / 𝑥 ] 𝜑 ↔ [ 𝑏 / 𝑥 ] 𝜑 ) ) ) )
15 eleq1 ⊢ ( 𝑏 = 𝐴 → ( 𝑏 ∈ ℤ ↔ 𝐴 ∈ ℤ ) )
16 breq2 ⊢ ( 𝑏 = 𝐴 → ( 0 ≤ 𝑏 ↔ 0 ≤ 𝐴 ) )
17 15 16 3anbi23d ⊢ ( 𝑏 = 𝐴 → ( ( 0 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 0 ≤ 𝑏 ) ↔ ( 0 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 0 ≤ 𝐴 ) ) )
18 dfsbcq ⊢ ( 𝑏 = 𝐴 → ( [ 𝑏 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
19 18 bibi2d ⊢ ( 𝑏 = 𝐴 → ( ( [ 0 / 𝑥 ] 𝜑 ↔ [ 𝑏 / 𝑥 ] 𝜑 ) ↔ ( [ 0 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) ) )
20 17 19 imbi12d ⊢ ( 𝑏 = 𝐴 → ( ( ( 0 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 0 ≤ 𝑏 ) → ( [ 0 / 𝑥 ] 𝜑 ↔ [ 𝑏 / 𝑥 ] 𝜑 ) ) ↔ ( ( 0 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 0 ≤ 𝐴 ) → ( [ 0 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) ) ) )
21 dfsbcq ⊢ ( 𝑎 = 𝑦 → ( [ 𝑎 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) )
22 21 bibi2d ⊢ ( 𝑎 = 𝑦 → ( ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑎 / 𝑥 ] 𝜑 ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) ) )
23 dfsbcq ⊢ ( 𝑎 = 𝑏 → ( [ 𝑎 / 𝑥 ] 𝜑 ↔ [ 𝑏 / 𝑥 ] 𝜑 ) )
24 23 bibi2d ⊢ ( 𝑎 = 𝑏 → ( ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑎 / 𝑥 ] 𝜑 ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑏 / 𝑥 ] 𝜑 ) ) )
25 dfsbcq ⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( [ 𝑎 / 𝑥 ] 𝜑 ↔ [ ( 𝑏 + 1 ) / 𝑥 ] 𝜑 ) )
26 25 bibi2d ⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑎 / 𝑥 ] 𝜑 ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ ( 𝑏 + 1 ) / 𝑥 ] 𝜑 ) ) )
27 biidd ⊢ ( 𝑦 ∈ ℤ → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) )
28 vex ⊢ 𝑦 ∈ V
29 28 2 sbcie ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 )
30 dfsbcq ⊢ ( 𝑦 = 𝑏 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑏 / 𝑥 ] 𝜑 ) )
31 29 30 bitr3id ⊢ ( 𝑦 = 𝑏 → ( 𝜓 ↔ [ 𝑏 / 𝑥 ] 𝜑 ) )
32 ovex ⊢ ( 𝑦 + 1 ) ∈ V
33 32 3 sbcie ⊢ ( [ ( 𝑦 + 1 ) / 𝑥 ] 𝜑 ↔ 𝜒 )
34 oveq1 ⊢ ( 𝑦 = 𝑏 → ( 𝑦 + 1 ) = ( 𝑏 + 1 ) )
35 34 sbceq1d ⊢ ( 𝑦 = 𝑏 → ( [ ( 𝑦 + 1 ) / 𝑥 ] 𝜑 ↔ [ ( 𝑏 + 1 ) / 𝑥 ] 𝜑 ) )
36 33 35 bitr3id ⊢ ( 𝑦 = 𝑏 → ( 𝜒 ↔ [ ( 𝑏 + 1 ) / 𝑥 ] 𝜑 ) )
37 31 36 bibi12d ⊢ ( 𝑦 = 𝑏 → ( ( 𝜓 ↔ 𝜒 ) ↔ ( [ 𝑏 / 𝑥 ] 𝜑 ↔ [ ( 𝑏 + 1 ) / 𝑥 ] 𝜑 ) ) )
38 37 1 vtoclga ⊢ ( 𝑏 ∈ ℤ → ( [ 𝑏 / 𝑥 ] 𝜑 ↔ [ ( 𝑏 + 1 ) / 𝑥 ] 𝜑 ) )
39 38 3ad2ant2 ⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝑦 ≤ 𝑏 ) → ( [ 𝑏 / 𝑥 ] 𝜑 ↔ [ ( 𝑏 + 1 ) / 𝑥 ] 𝜑 ) )
40 39 bibi2d ⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝑦 ≤ 𝑏 ) → ( ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑏 / 𝑥 ] 𝜑 ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ ( 𝑏 + 1 ) / 𝑥 ] 𝜑 ) ) )
41 40 biimpd ⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝑦 ≤ 𝑏 ) → ( ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑏 / 𝑥 ] 𝜑 ) → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ ( 𝑏 + 1 ) / 𝑥 ] 𝜑 ) ) )
42 22 24 26 24 27 41 uzind ⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝑦 ≤ 𝑏 ) → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑏 / 𝑥 ] 𝜑 ) )
43 14 20 42 vtocl2g ⊢ ( ( 0 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( ( 0 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 0 ≤ 𝐴 ) → ( [ 0 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) ) )
44 43 3adant3 ⊢ ( ( 0 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 0 ≤ 𝐴 ) → ( ( 0 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 0 ≤ 𝐴 ) → ( [ 0 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) ) )
45 44 pm2.43i ⊢ ( ( 0 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 0 ≤ 𝐴 ) → ( [ 0 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
46 8 45 mp3an1 ⊢ ( ( 𝐴 ∈ ℤ ∧ 0 ≤ 𝐴 ) → ( [ 0 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
47 eleq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∈ ℤ ↔ 𝐴 ∈ ℤ ) )
48 breq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ≤ 𝑏 ↔ 𝐴 ≤ 𝑏 ) )
49 47 48 3anbi13d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝑦 ≤ 𝑏 ) ↔ ( 𝐴 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝐴 ≤ 𝑏 ) ) )
50 dfsbcq ⊢ ( 𝑦 = 𝐴 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
51 50 bibi1d ⊢ ( 𝑦 = 𝐴 → ( ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑏 / 𝑥 ] 𝜑 ) ↔ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ [ 𝑏 / 𝑥 ] 𝜑 ) ) )
52 49 51 imbi12d ⊢ ( 𝑦 = 𝐴 → ( ( ( 𝑦 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝑦 ≤ 𝑏 ) → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑏 / 𝑥 ] 𝜑 ) ) ↔ ( ( 𝐴 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝐴 ≤ 𝑏 ) → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ [ 𝑏 / 𝑥 ] 𝜑 ) ) ) )
53 eleq1 ⊢ ( 𝑏 = 0 → ( 𝑏 ∈ ℤ ↔ 0 ∈ ℤ ) )
54 breq2 ⊢ ( 𝑏 = 0 → ( 𝐴 ≤ 𝑏 ↔ 𝐴 ≤ 0 ) )
55 53 54 3anbi23d ⊢ ( 𝑏 = 0 → ( ( 𝐴 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝐴 ≤ 𝑏 ) ↔ ( 𝐴 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝐴 ≤ 0 ) ) )
56 dfsbcq ⊢ ( 𝑏 = 0 → ( [ 𝑏 / 𝑥 ] 𝜑 ↔ [ 0 / 𝑥 ] 𝜑 ) )
57 56 bibi2d ⊢ ( 𝑏 = 0 → ( ( [ 𝐴 / 𝑥 ] 𝜑 ↔ [ 𝑏 / 𝑥 ] 𝜑 ) ↔ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ [ 0 / 𝑥 ] 𝜑 ) ) )
58 55 57 imbi12d ⊢ ( 𝑏 = 0 → ( ( ( 𝐴 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝐴 ≤ 𝑏 ) → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ [ 𝑏 / 𝑥 ] 𝜑 ) ) ↔ ( ( 𝐴 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝐴 ≤ 0 ) → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ [ 0 / 𝑥 ] 𝜑 ) ) ) )
59 52 58 42 vtocl2g ⊢ ( ( 𝐴 ∈ ℤ ∧ 0 ∈ ℤ ) → ( ( 𝐴 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝐴 ≤ 0 ) → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ [ 0 / 𝑥 ] 𝜑 ) ) )
60 59 3adant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝐴 ≤ 0 ) → ( ( 𝐴 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝐴 ≤ 0 ) → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ [ 0 / 𝑥 ] 𝜑 ) ) )
61 60 pm2.43i ⊢ ( ( 𝐴 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝐴 ≤ 0 ) → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ [ 0 / 𝑥 ] 𝜑 ) )
62 8 61 mp3an2 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≤ 0 ) → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ [ 0 / 𝑥 ] 𝜑 ) )
63 62 bicomd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≤ 0 ) → ( [ 0 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
64 0re ⊢ 0 ∈ ℝ
65 zre ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
66 letric ⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 0 ≤ 𝐴 ∨ 𝐴 ≤ 0 ) )
67 64 65 66 sylancr ⊢ ( 𝐴 ∈ ℤ → ( 0 ≤ 𝐴 ∨ 𝐴 ≤ 0 ) )
68 46 63 67 mpjaodan ⊢ ( 𝐴 ∈ ℤ → ( [ 0 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
69 7 68 bitr3id ⊢ ( 𝐴 ∈ ℤ → ( 𝜃 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
70 5 sbcieg ⊢ ( 𝐴 ∈ ℤ → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝜏 ) )
71 69 70 bitrd ⊢ ( 𝐴 ∈ ℤ → ( 𝜃 ↔ 𝜏 ) )