Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  iseqf1olemab GIF version

Theorem iseqf1olemab 10322
 Description: Lemma for seq3f1o 10337. (Contributed by Jim Kingdon, 27-Aug-2022.)
Hypotheses
Ref Expression
iseqf1olemqcl.k (𝜑𝐾 ∈ (𝑀...𝑁))
iseqf1olemqcl.j (𝜑𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
iseqf1olemqcl.a (𝜑𝐴 ∈ (𝑀...𝑁))
iseqf1olemnab.b (𝜑𝐵 ∈ (𝑀...𝑁))
iseqf1olemnab.eq (𝜑 → (𝑄𝐴) = (𝑄𝐵))
iseqf1olemnab.q 𝑄 = (𝑢 ∈ (𝑀...𝑁) ↦ if(𝑢 ∈ (𝐾...(𝐽𝐾)), if(𝑢 = 𝐾, 𝐾, (𝐽‘(𝑢 − 1))), (𝐽𝑢)))
iseqf1olemab.a (𝜑𝐴 ∈ (𝐾...(𝐽𝐾)))
iseqf1olemab.b (𝜑𝐵 ∈ (𝐾...(𝐽𝐾)))
Assertion
Ref Expression
iseqf1olemab (𝜑𝐴 = 𝐵)
Distinct variable groups:   𝑢,𝐴   𝑢,𝐵   𝑢,𝐽   𝑢,𝐾   𝑢,𝑀   𝑢,𝑁
Allowed substitution hints:   𝜑(𝑢)   𝑄(𝑢)

Proof of Theorem iseqf1olemab
StepHypRef Expression
1 eqtr3 2161 . . . . 5 ((𝐵 = 𝐾𝐴 = 𝐾) → 𝐵 = 𝐴)
21eqcomd 2147 . . . 4 ((𝐵 = 𝐾𝐴 = 𝐾) → 𝐴 = 𝐵)
32adantll 468 . . 3 (((𝜑𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → 𝐴 = 𝐵)
4 iseqf1olemqcl.a . . . . . . . 8 (𝜑𝐴 ∈ (𝑀...𝑁))
5 elfzelz 9866 . . . . . . . 8 (𝐴 ∈ (𝑀...𝑁) → 𝐴 ∈ ℤ)
64, 5syl 14 . . . . . . 7 (𝜑𝐴 ∈ ℤ)
76zred 9226 . . . . . 6 (𝜑𝐴 ∈ ℝ)
87ltm1d 8743 . . . . 5 (𝜑 → (𝐴 − 1) < 𝐴)
98ad2antrr 480 . . . 4 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝐴 − 1) < 𝐴)
107ad2antrr 480 . . . . 5 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → 𝐴 ∈ ℝ)
11 peano2rem 8082 . . . . . 6 (𝐴 ∈ ℝ → (𝐴 − 1) ∈ ℝ)
1210, 11syl 14 . . . . 5 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝐴 − 1) ∈ ℝ)
13 iseqf1olemab.a . . . . . . . 8 (𝜑𝐴 ∈ (𝐾...(𝐽𝐾)))
14 elfzle2 9868 . . . . . . . 8 (𝐴 ∈ (𝐾...(𝐽𝐾)) → 𝐴 ≤ (𝐽𝐾))
1513, 14syl 14 . . . . . . 7 (𝜑𝐴 ≤ (𝐽𝐾))
1615ad2antrr 480 . . . . . 6 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → 𝐴 ≤ (𝐽𝐾))
17 iseqf1olemqcl.k . . . . . . . . . . . 12 (𝜑𝐾 ∈ (𝑀...𝑁))
18 iseqf1olemqcl.j . . . . . . . . . . . 12 (𝜑𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
19 iseqf1olemnab.q . . . . . . . . . . . 12 𝑄 = (𝑢 ∈ (𝑀...𝑁) ↦ if(𝑢 ∈ (𝐾...(𝐽𝐾)), if(𝑢 = 𝐾, 𝐾, (𝐽‘(𝑢 − 1))), (𝐽𝑢)))
2017, 18, 4, 19iseqf1olemqval 10320 . . . . . . . . . . 11 (𝜑 → (𝑄𝐴) = if(𝐴 ∈ (𝐾...(𝐽𝐾)), if(𝐴 = 𝐾, 𝐾, (𝐽‘(𝐴 − 1))), (𝐽𝐴)))
2113iftrued 3488 . . . . . . . . . . 11 (𝜑 → if(𝐴 ∈ (𝐾...(𝐽𝐾)), if(𝐴 = 𝐾, 𝐾, (𝐽‘(𝐴 − 1))), (𝐽𝐴)) = if(𝐴 = 𝐾, 𝐾, (𝐽‘(𝐴 − 1))))
2220, 21eqtrd 2174 . . . . . . . . . 10 (𝜑 → (𝑄𝐴) = if(𝐴 = 𝐾, 𝐾, (𝐽‘(𝐴 − 1))))
2322ad2antrr 480 . . . . . . . . 9 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝑄𝐴) = if(𝐴 = 𝐾, 𝐾, (𝐽‘(𝐴 − 1))))
24 iseqf1olemnab.eq . . . . . . . . . . 11 (𝜑 → (𝑄𝐴) = (𝑄𝐵))
2524ad2antrr 480 . . . . . . . . . 10 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝑄𝐴) = (𝑄𝐵))
26 iseqf1olemnab.b . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ (𝑀...𝑁))
2717, 18, 26, 19iseqf1olemqval 10320 . . . . . . . . . . . . 13 (𝜑 → (𝑄𝐵) = if(𝐵 ∈ (𝐾...(𝐽𝐾)), if(𝐵 = 𝐾, 𝐾, (𝐽‘(𝐵 − 1))), (𝐽𝐵)))
28 iseqf1olemab.b . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ (𝐾...(𝐽𝐾)))
2928iftrued 3488 . . . . . . . . . . . . 13 (𝜑 → if(𝐵 ∈ (𝐾...(𝐽𝐾)), if(𝐵 = 𝐾, 𝐾, (𝐽‘(𝐵 − 1))), (𝐽𝐵)) = if(𝐵 = 𝐾, 𝐾, (𝐽‘(𝐵 − 1))))
3027, 29eqtrd 2174 . . . . . . . . . . . 12 (𝜑 → (𝑄𝐵) = if(𝐵 = 𝐾, 𝐾, (𝐽‘(𝐵 − 1))))
3130ad2antrr 480 . . . . . . . . . . 11 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝑄𝐵) = if(𝐵 = 𝐾, 𝐾, (𝐽‘(𝐵 − 1))))
32 simplr 520 . . . . . . . . . . . 12 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → 𝐵 = 𝐾)
3332iftrued 3488 . . . . . . . . . . 11 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → if(𝐵 = 𝐾, 𝐾, (𝐽‘(𝐵 − 1))) = 𝐾)
3431, 33eqtrd 2174 . . . . . . . . . 10 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝑄𝐵) = 𝐾)
3525, 34eqtrd 2174 . . . . . . . . 9 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝑄𝐴) = 𝐾)
36 simpr 109 . . . . . . . . . 10 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → ¬ 𝐴 = 𝐾)
3736iffalsed 3491 . . . . . . . . 9 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → if(𝐴 = 𝐾, 𝐾, (𝐽‘(𝐴 − 1))) = (𝐽‘(𝐴 − 1)))
3823, 35, 373eqtr3d 2182 . . . . . . . 8 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → 𝐾 = (𝐽‘(𝐴 − 1)))
3938fveq2d 5437 . . . . . . 7 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝐽𝐾) = (𝐽‘(𝐽‘(𝐴 − 1))))
4018ad2antrr 480 . . . . . . . 8 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
41 elfzel1 9865 . . . . . . . . . . . . 13 (𝐾 ∈ (𝑀...𝑁) → 𝑀 ∈ ℤ)
4217, 41syl 14 . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℤ)
43 elfzel2 9864 . . . . . . . . . . . . 13 (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ ℤ)
4417, 43syl 14 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℤ)
45 peano2zm 9145 . . . . . . . . . . . . 13 (𝐴 ∈ ℤ → (𝐴 − 1) ∈ ℤ)
466, 45syl 14 . . . . . . . . . . . 12 (𝜑 → (𝐴 − 1) ∈ ℤ)
4742, 44, 463jca 1162 . . . . . . . . . . 11 (𝜑 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐴 − 1) ∈ ℤ))
4847adantr 274 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐴 − 1) ∈ ℤ))
4942zred 9226 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ ℝ)
5049adantr 274 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → 𝑀 ∈ ℝ)
51 elfzelz 9866 . . . . . . . . . . . . . . 15 (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ ℤ)
5217, 51syl 14 . . . . . . . . . . . . . 14 (𝜑𝐾 ∈ ℤ)
5352zred 9226 . . . . . . . . . . . . 13 (𝜑𝐾 ∈ ℝ)
5453adantr 274 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → 𝐾 ∈ ℝ)
5546zred 9226 . . . . . . . . . . . . 13 (𝜑 → (𝐴 − 1) ∈ ℝ)
5655adantr 274 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → (𝐴 − 1) ∈ ℝ)
57 elfzle1 9867 . . . . . . . . . . . . . 14 (𝐾 ∈ (𝑀...𝑁) → 𝑀𝐾)
5817, 57syl 14 . . . . . . . . . . . . 13 (𝜑𝑀𝐾)
5958adantr 274 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → 𝑀𝐾)
60 simpr 109 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → ¬ 𝐴 = 𝐾)
61 eqcom 2143 . . . . . . . . . . . . . . 15 (𝐴 = 𝐾𝐾 = 𝐴)
6260, 61sylnib 666 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → ¬ 𝐾 = 𝐴)
63 elfzle1 9867 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ (𝐾...(𝐽𝐾)) → 𝐾𝐴)
6413, 63syl 14 . . . . . . . . . . . . . . . 16 (𝜑𝐾𝐴)
65 zleloe 9154 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝐾𝐴 ↔ (𝐾 < 𝐴𝐾 = 𝐴)))
6652, 6, 65syl2anc 409 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐾𝐴 ↔ (𝐾 < 𝐴𝐾 = 𝐴)))
6764, 66mpbid 146 . . . . . . . . . . . . . . 15 (𝜑 → (𝐾 < 𝐴𝐾 = 𝐴))
6867adantr 274 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → (𝐾 < 𝐴𝐾 = 𝐴))
6962, 68ecased 1328 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → 𝐾 < 𝐴)
70 zltlem1 9164 . . . . . . . . . . . . . . 15 ((𝐾 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝐾 < 𝐴𝐾 ≤ (𝐴 − 1)))
7152, 6, 70syl2anc 409 . . . . . . . . . . . . . 14 (𝜑 → (𝐾 < 𝐴𝐾 ≤ (𝐴 − 1)))
7271adantr 274 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → (𝐾 < 𝐴𝐾 ≤ (𝐴 − 1)))
7369, 72mpbid 146 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → 𝐾 ≤ (𝐴 − 1))
7450, 54, 56, 59, 73letrd 7939 . . . . . . . . . . 11 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → 𝑀 ≤ (𝐴 − 1))
757adantr 274 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → 𝐴 ∈ ℝ)
7644zred 9226 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℝ)
7776adantr 274 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → 𝑁 ∈ ℝ)
7875lem1d 8744 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → (𝐴 − 1) ≤ 𝐴)
79 elfzle2 9868 . . . . . . . . . . . . . 14 (𝐴 ∈ (𝑀...𝑁) → 𝐴𝑁)
804, 79syl 14 . . . . . . . . . . . . 13 (𝜑𝐴𝑁)
8180adantr 274 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → 𝐴𝑁)
8256, 75, 77, 78, 81letrd 7939 . . . . . . . . . . 11 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → (𝐴 − 1) ≤ 𝑁)
8374, 82jca 304 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → (𝑀 ≤ (𝐴 − 1) ∧ (𝐴 − 1) ≤ 𝑁))
84 elfz2 9857 . . . . . . . . . 10 ((𝐴 − 1) ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐴 − 1) ∈ ℤ) ∧ (𝑀 ≤ (𝐴 − 1) ∧ (𝐴 − 1) ≤ 𝑁)))
8548, 83, 84sylanbrc 414 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → (𝐴 − 1) ∈ (𝑀...𝑁))
8685adantlr 469 . . . . . . . 8 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝐴 − 1) ∈ (𝑀...𝑁))
87 f1ocnvfv1 5690 . . . . . . . 8 ((𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ (𝐴 − 1) ∈ (𝑀...𝑁)) → (𝐽‘(𝐽‘(𝐴 − 1))) = (𝐴 − 1))
8840, 86, 87syl2anc 409 . . . . . . 7 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝐽‘(𝐽‘(𝐴 − 1))) = (𝐴 − 1))
8939, 88eqtrd 2174 . . . . . 6 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝐽𝐾) = (𝐴 − 1))
9016, 89breqtrd 3964 . . . . 5 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → 𝐴 ≤ (𝐴 − 1))
9110, 12, 90lensymd 7937 . . . 4 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → ¬ (𝐴 − 1) < 𝐴)
929, 91pm2.21dd 610 . . 3 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → 𝐴 = 𝐵)
93 zdceq 9179 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝐾 ∈ ℤ) → DECID 𝐴 = 𝐾)
946, 52, 93syl2anc 409 . . . . 5 (𝜑DECID 𝐴 = 𝐾)
95 exmiddc 822 . . . . 5 (DECID 𝐴 = 𝐾 → (𝐴 = 𝐾 ∨ ¬ 𝐴 = 𝐾))
9694, 95syl 14 . . . 4 (𝜑 → (𝐴 = 𝐾 ∨ ¬ 𝐴 = 𝐾))
9796adantr 274 . . 3 ((𝜑𝐵 = 𝐾) → (𝐴 = 𝐾 ∨ ¬ 𝐴 = 𝐾))
983, 92, 97mpjaodan 788 . 2 ((𝜑𝐵 = 𝐾) → 𝐴 = 𝐵)
99 elfzelz 9866 . . . . . . . 8 (𝐵 ∈ (𝑀...𝑁) → 𝐵 ∈ ℤ)
10026, 99syl 14 . . . . . . 7 (𝜑𝐵 ∈ ℤ)
101100zred 9226 . . . . . 6 (𝜑𝐵 ∈ ℝ)
102101ltm1d 8743 . . . . 5 (𝜑 → (𝐵 − 1) < 𝐵)
103102ad2antrr 480 . . . 4 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → (𝐵 − 1) < 𝐵)
104101ad2antrr 480 . . . . 5 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → 𝐵 ∈ ℝ)
105 peano2rem 8082 . . . . . 6 (𝐵 ∈ ℝ → (𝐵 − 1) ∈ ℝ)
106104, 105syl 14 . . . . 5 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → (𝐵 − 1) ∈ ℝ)
107 elfzle2 9868 . . . . . . . 8 (𝐵 ∈ (𝐾...(𝐽𝐾)) → 𝐵 ≤ (𝐽𝐾))
10828, 107syl 14 . . . . . . 7 (𝜑𝐵 ≤ (𝐽𝐾))
109108ad2antrr 480 . . . . . 6 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → 𝐵 ≤ (𝐽𝐾))
11030ad2antrr 480 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → (𝑄𝐵) = if(𝐵 = 𝐾, 𝐾, (𝐽‘(𝐵 − 1))))
11124eqcomd 2147 . . . . . . . . . . 11 (𝜑 → (𝑄𝐵) = (𝑄𝐴))
112111ad2antrr 480 . . . . . . . . . 10 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → (𝑄𝐵) = (𝑄𝐴))
11322ad2antrr 480 . . . . . . . . . . 11 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → (𝑄𝐴) = if(𝐴 = 𝐾, 𝐾, (𝐽‘(𝐴 − 1))))
114 simpr 109 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → 𝐴 = 𝐾)
115114iftrued 3488 . . . . . . . . . . 11 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → if(𝐴 = 𝐾, 𝐾, (𝐽‘(𝐴 − 1))) = 𝐾)
116113, 115eqtrd 2174 . . . . . . . . . 10 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → (𝑄𝐴) = 𝐾)
117112, 116eqtrd 2174 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → (𝑄𝐵) = 𝐾)
118 simplr 520 . . . . . . . . . 10 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → ¬ 𝐵 = 𝐾)
119118iffalsed 3491 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → if(𝐵 = 𝐾, 𝐾, (𝐽‘(𝐵 − 1))) = (𝐽‘(𝐵 − 1)))
120110, 117, 1193eqtr3d 2182 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → 𝐾 = (𝐽‘(𝐵 − 1)))
121120fveq2d 5437 . . . . . . 7 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → (𝐽𝐾) = (𝐽‘(𝐽‘(𝐵 − 1))))
12218ad2antrr 480 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
123 peano2zm 9145 . . . . . . . . . . . . 13 (𝐵 ∈ ℤ → (𝐵 − 1) ∈ ℤ)
124100, 123syl 14 . . . . . . . . . . . 12 (𝜑 → (𝐵 − 1) ∈ ℤ)
12542, 44, 1243jca 1162 . . . . . . . . . . 11 (𝜑 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐵 − 1) ∈ ℤ))
126125adantr 274 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐵 − 1) ∈ ℤ))
12749adantr 274 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → 𝑀 ∈ ℝ)
12853adantr 274 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → 𝐾 ∈ ℝ)
129101, 105syl 14 . . . . . . . . . . . . 13 (𝜑 → (𝐵 − 1) ∈ ℝ)
130129adantr 274 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → (𝐵 − 1) ∈ ℝ)
13158adantr 274 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → 𝑀𝐾)
132 simpr 109 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → ¬ 𝐵 = 𝐾)
133 eqcom 2143 . . . . . . . . . . . . . . 15 (𝐵 = 𝐾𝐾 = 𝐵)
134132, 133sylnib 666 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → ¬ 𝐾 = 𝐵)
135 elfzle1 9867 . . . . . . . . . . . . . . . . 17 (𝐵 ∈ (𝐾...(𝐽𝐾)) → 𝐾𝐵)
13628, 135syl 14 . . . . . . . . . . . . . . . 16 (𝜑𝐾𝐵)
137136adantr 274 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → 𝐾𝐵)
138 zleloe 9154 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐾𝐵 ↔ (𝐾 < 𝐵𝐾 = 𝐵)))
13952, 100, 138syl2anc 409 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐾𝐵 ↔ (𝐾 < 𝐵𝐾 = 𝐵)))
140139adantr 274 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → (𝐾𝐵 ↔ (𝐾 < 𝐵𝐾 = 𝐵)))
141137, 140mpbid 146 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → (𝐾 < 𝐵𝐾 = 𝐵))
142134, 141ecased 1328 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → 𝐾 < 𝐵)
143 zltlem1 9164 . . . . . . . . . . . . . . 15 ((𝐾 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐾 < 𝐵𝐾 ≤ (𝐵 − 1)))
14452, 100, 143syl2anc 409 . . . . . . . . . . . . . 14 (𝜑 → (𝐾 < 𝐵𝐾 ≤ (𝐵 − 1)))
145144adantr 274 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → (𝐾 < 𝐵𝐾 ≤ (𝐵 − 1)))
146142, 145mpbid 146 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → 𝐾 ≤ (𝐵 − 1))
147127, 128, 130, 131, 146letrd 7939 . . . . . . . . . . 11 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → 𝑀 ≤ (𝐵 − 1))
148101lem1d 8744 . . . . . . . . . . . . 13 (𝜑 → (𝐵 − 1) ≤ 𝐵)
149 elfzle2 9868 . . . . . . . . . . . . . 14 (𝐵 ∈ (𝑀...𝑁) → 𝐵𝑁)
15026, 149syl 14 . . . . . . . . . . . . 13 (𝜑𝐵𝑁)
151129, 101, 76, 148, 150letrd 7939 . . . . . . . . . . . 12 (𝜑 → (𝐵 − 1) ≤ 𝑁)
152151adantr 274 . . . . . . . . . . 11 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → (𝐵 − 1) ≤ 𝑁)
153147, 152jca 304 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → (𝑀 ≤ (𝐵 − 1) ∧ (𝐵 − 1) ≤ 𝑁))
154 elfz2 9857 . . . . . . . . . 10 ((𝐵 − 1) ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐵 − 1) ∈ ℤ) ∧ (𝑀 ≤ (𝐵 − 1) ∧ (𝐵 − 1) ≤ 𝑁)))
155126, 153, 154sylanbrc 414 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → (𝐵 − 1) ∈ (𝑀...𝑁))
156155adantr 274 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → (𝐵 − 1) ∈ (𝑀...𝑁))
157 f1ocnvfv1 5690 . . . . . . . 8 ((𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ (𝐵 − 1) ∈ (𝑀...𝑁)) → (𝐽‘(𝐽‘(𝐵 − 1))) = (𝐵 − 1))
158122, 156, 157syl2anc 409 . . . . . . 7 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → (𝐽‘(𝐽‘(𝐵 − 1))) = (𝐵 − 1))
159121, 158eqtrd 2174 . . . . . 6 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → (𝐽𝐾) = (𝐵 − 1))
160109, 159breqtrd 3964 . . . . 5 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → 𝐵 ≤ (𝐵 − 1))
161104, 106, 160lensymd 7937 . . . 4 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → ¬ (𝐵 − 1) < 𝐵)
162103, 161pm2.21dd 610 . . 3 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → 𝐴 = 𝐵)
1636zcnd 9227 . . . . 5 (𝜑𝐴 ∈ ℂ)
164163ad2antrr 480 . . . 4 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → 𝐴 ∈ ℂ)
165100zcnd 9227 . . . . 5 (𝜑𝐵 ∈ ℂ)
166165ad2antrr 480 . . . 4 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → 𝐵 ∈ ℂ)
167 1cnd 7835 . . . 4 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → 1 ∈ ℂ)
16824ad2antrr 480 . . . . . 6 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝑄𝐴) = (𝑄𝐵))
16922ad2antrr 480 . . . . . . 7 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝑄𝐴) = if(𝐴 = 𝐾, 𝐾, (𝐽‘(𝐴 − 1))))
170 simpr 109 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → ¬ 𝐴 = 𝐾)
171170iffalsed 3491 . . . . . . 7 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → if(𝐴 = 𝐾, 𝐾, (𝐽‘(𝐴 − 1))) = (𝐽‘(𝐴 − 1)))
172169, 171eqtrd 2174 . . . . . 6 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝑄𝐴) = (𝐽‘(𝐴 − 1)))
17330ad2antrr 480 . . . . . . 7 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝑄𝐵) = if(𝐵 = 𝐾, 𝐾, (𝐽‘(𝐵 − 1))))
174 simplr 520 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → ¬ 𝐵 = 𝐾)
175174iffalsed 3491 . . . . . . 7 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → if(𝐵 = 𝐾, 𝐾, (𝐽‘(𝐵 − 1))) = (𝐽‘(𝐵 − 1)))
176173, 175eqtrd 2174 . . . . . 6 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝑄𝐵) = (𝐽‘(𝐵 − 1)))
177168, 172, 1763eqtr3d 2182 . . . . 5 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝐽‘(𝐴 − 1)) = (𝐽‘(𝐵 − 1)))
178 f1of1 5378 . . . . . . . 8 (𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) → 𝐽:(𝑀...𝑁)–1-1→(𝑀...𝑁))
17918, 178syl 14 . . . . . . 7 (𝜑𝐽:(𝑀...𝑁)–1-1→(𝑀...𝑁))
180179ad2antrr 480 . . . . . 6 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → 𝐽:(𝑀...𝑁)–1-1→(𝑀...𝑁))
18185adantlr 469 . . . . . 6 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝐴 − 1) ∈ (𝑀...𝑁))
182155adantr 274 . . . . . 6 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝐵 − 1) ∈ (𝑀...𝑁))
183 f1veqaeq 5682 . . . . . 6 ((𝐽:(𝑀...𝑁)–1-1→(𝑀...𝑁) ∧ ((𝐴 − 1) ∈ (𝑀...𝑁) ∧ (𝐵 − 1) ∈ (𝑀...𝑁))) → ((𝐽‘(𝐴 − 1)) = (𝐽‘(𝐵 − 1)) → (𝐴 − 1) = (𝐵 − 1)))
184180, 181, 182, 183syl12anc 1215 . . . . 5 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → ((𝐽‘(𝐴 − 1)) = (𝐽‘(𝐵 − 1)) → (𝐴 − 1) = (𝐵 − 1)))
185177, 184mpd 13 . . . 4 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝐴 − 1) = (𝐵 − 1))
186164, 166, 167, 185subcan2d 8168 . . 3 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → 𝐴 = 𝐵)
18796adantr 274 . . 3 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → (𝐴 = 𝐾 ∨ ¬ 𝐴 = 𝐾))
188162, 186, 187mpjaodan 788 . 2 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → 𝐴 = 𝐵)
189 zdceq 9179 . . . 4 ((𝐵 ∈ ℤ ∧ 𝐾 ∈ ℤ) → DECID 𝐵 = 𝐾)
190100, 52, 189syl2anc 409 . . 3 (𝜑DECID 𝐵 = 𝐾)
191 exmiddc 822 . . 3 (DECID 𝐵 = 𝐾 → (𝐵 = 𝐾 ∨ ¬ 𝐵 = 𝐾))
192190, 191syl 14 . 2 (𝜑 → (𝐵 = 𝐾 ∨ ¬ 𝐵 = 𝐾))
19398, 188, 192mpjaodan 788 1 (𝜑𝐴 = 𝐵)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 698  DECID wdc 820   ∧ w3a 963   = wceq 1332   ∈ wcel 1481  ifcif 3481   class class class wbr 3939   ↦ cmpt 3999  ◡ccnv 4550  –1-1→wf1 5132  –1-1-onto→wf1o 5134  ‘cfv 5135  (class class class)co 5786  ℂcc 7671  ℝcr 7672  1c1 7674   < clt 7853   ≤ cle 7854   − cmin 7986  ℤcz 9107  ...cfz 9850 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2123  ax-sep 4056  ax-pow 4108  ax-pr 4142  ax-un 4366  ax-setind 4463  ax-cnex 7764  ax-resscn 7765  ax-1cn 7766  ax-1re 7767  ax-icn 7768  ax-addcl 7769  ax-addrcl 7770  ax-mulcl 7771  ax-addcom 7773  ax-addass 7775  ax-distr 7777  ax-i2m1 7778  ax-0lt1 7779  ax-0id 7781  ax-rnegex 7782  ax-cnre 7784  ax-pre-ltirr 7785  ax-pre-ltwlin 7786  ax-pre-lttrn 7787  ax-pre-ltadd 7789 This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1738  df-eu 2004  df-mo 2005  df-clab 2128  df-cleq 2134  df-clel 2137  df-nfc 2272  df-ne 2311  df-nel 2406  df-ral 2423  df-rex 2424  df-reu 2425  df-rab 2427  df-v 2693  df-sbc 2916  df-dif 3080  df-un 3082  df-in 3084  df-ss 3091  df-if 3482  df-pw 3519  df-sn 3540  df-pr 3541  df-op 3543  df-uni 3747  df-int 3782  df-br 3940  df-opab 4000  df-mpt 4001  df-id 4226  df-xp 4557  df-rel 4558  df-cnv 4559  df-co 4560  df-dm 4561  df-rn 4562  df-res 4563  df-ima 4564  df-iota 5100  df-fun 5137  df-fn 5138  df-f 5139  df-f1 5140  df-fo 5141  df-f1o 5142  df-fv 5143  df-riota 5742  df-ov 5789  df-oprab 5790  df-mpo 5791  df-pnf 7855  df-mnf 7856  df-xr 7857  df-ltxr 7858  df-le 7859  df-sub 7988  df-neg 7989  df-inn 8774  df-n0 9031  df-z 9108  df-uz 9380  df-fz 9851 This theorem is referenced by:  iseqf1olemmo  10325
 Copyright terms: Public domain W3C validator